2024.07.10
https://gyazo.com/4eb94dd5087e80fa0a30f8226ce1fab5
証明可能性論理$ \bf GLのKripke弱完全性/有限フレーム性:推移的かつ非反射的な有限フレームクラスに対して完全:を形式化した.
これはかなりやりやすい証明だった.なぜなら(素朴な)極大無矛盾集合に関する性質だけで済むので 他の証明は部分論理式集合の部分集合であるなどの制約を課すためもう一度諸々証明が必要で,やや面倒.
memo
スマートコントラクトで形式検証が(観測する分には)盛んな理由として,一回デプロイすると基本的に修正不能だからなるべくデプロイ前に厳密に検証しておきたいという要請があるから,という話を聞いた. 確かに