昨日から情報証明論をやっている。
http://markun.cs.shinshu-u.ac.jp/learn/iproof/index-j.html

Mizarという、よくわからない難しい言語である。
電子工作で74シリーズとか使う人には、論理チェックをしてくれるので、
設計の支援になりそうな感じがする。

で、テストをやってみた。
以前やってみて意味がわからず「あっ!」というまでもなく挫折したけど、
アプローチの仕方を変えてみることにした。

理学的に落ち着いてこんこんと考えるスタイルから、
とりあえずCAIクリアできればいいか。と気軽に取り組んでみたのである。

そうしたら、ある程度は進むことができた。
なんだかんだでやっていくうちに、少しずつ分かってきた感じがする。
でも、CAIのテストが何かバグがあるような気がする。

問題文が表示されない 答えに1765と入力すればOK
プログラムに()を付けるとエラーになる。 きめ打ちしているっぽい。これは明らかにCAIプログラムの手抜き。
アンパサンドの周りにスペースを入れると、エラーになる。 これも決め打ちしているからこうなる。パースする際にスペースをトークナイザに入れてしまうだけでいいと思うんだが・・

で、結構さくさく進み、4章のNo7で詰まる。ので飛ばして次々行き、4章以外のすべてのCAIを修了した。
第8章が反映されないのが、ものすごく気になるけど。

で、また4章に戻ってきた。
Are the following three logical formulae mutually disjoint? Input yes or no : $a & not($b & $c );
($a&$b&$c);
($a¬($b or$c));

さっぱりわからない。
$a & not($b & $c ) & ($a&$b&$c) & ($a¬($b or$c)) iff contradiction;
でMizarでチェックをかけると、うまくいくので、 noと入力してもyesといわれる・・・。

全くわからないので最後の手段に出る。
絨毯爆撃である。何故絨毯というんだろう。

expression1 expression2 expression3 Answer
$a & $b or $c $a & not $c $b & not($a or $c) no
$a & not $c $c & not($a or $b) $b & not($a or $c) yes
($c & not($a or $b)) ($b & not($a or $c)) ($a & not $c) yes
$c or not($a & $b) $b & not($a or $c) $a & not($b or $c) no
($a & $c) ($a & not($b or $c)) ($b or $c) not $a yes
$a & not($b or $c ) (($b or $c )¬$a) ($a&$c) yes
$a & not($b or $c); $a & not($b & $c); $a & $b & $c no
$a & not($b & $c); $a & $b & $c; $a & not($b or $c); no
$a & $b & $c $b & not($a or $c); $a & not $c; yes
$b & not($a or $c); $a & not($b or $c); $c or not($a & $b); no