IsabelleによるCBC CasperのSafetyの証明をしました
日記です。 リポジトリ: LayerXcom/cbc-casper-proof 概要 (私は LayerX の人ではないですが)LayerX 社の人と色々あって CBC Casper というブロックチェーンのプロトコルの検証作業を行いました。(主に定理証明士としてのお手伝い) 半年くらいかかったけどやりたかった証明についにたどり着いたよという話。 CBC Casper って何 わからん。(無知) 何かブロックチェーンのプロトコルの名前らしい。Ethereum 財団が目をつけてるらしい。いわゆるビットコインとは違ってブロックを頑張ってマシンをぶん回してマイニングしたりしないらしい(ビットコインは PoW で CBC Casper は PoS)。 詳しいことは詳しい人に聞いたほうがいいよ(真理)。 cf: CBC Casper と形式的検証 Isabelle で検証って何するの ブロックチェー
Post correspondence problem - Wikipedia
Not to be confused with the other Post's problem on the existence of incomparable r.e. Turing degrees. The Post correspondence problem is an undecidable decision problem that was introduced by Emil Post in 1946.[1] Because it is simpler than the halting problem and the Entscheidungsproblem it is often used in proofs of undecidability. Definition of the problem[edit] Let be an alphabet with at leas
Write Yourself a Theorem Prover in 48 Hours (その1) - Qiita
この記事は定理証明アドベントカレンダー2013のたぶん7日目の記事です 誰でも定理証明器を作れるようになろうという趣旨です。ここではCoqのパクリみたいなサブセットを48時間で作ります。 タイトルの元ネタは http://en.wikibooks.org/wiki/Write_Yourself_a_Scheme_in_48_Hours です。というわけで、使う言語はHaskellですが、他の言語でも特に問題ないと思います。 定理証明器の部品は以下のものが必要です。 記述言語 カーネル 証明支援言語 その他 記述言語はCoqではGallinaといわれてる部分です。立派なプログラミング言語をひとつ設計しないといけません。このプログラミング言語によって、定理のステートメントを記述したり、証明を記述したり、関数を書いたり、データ構造を定義したりします。 カーネルは記述言語のインタープリタになります
ソフトウェア科学特論: 命題論理
本Webページ(およびPDF)の作成には Emacs org-mode を用いており， 数式等の表示は MathJax を用いています． IEでは正しく表示されないことがあるため， Firefox, Safari等のWebブラウザでJavaScriptを有効にしてお使いください． また org-info.js を利用しており， 「m」キーをタイプするとinfoモードでの表示になります． 利用できるショートカットは「?」で表示されます．
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Criterion -- from Wolfram MathWorld
