■

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

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

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

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

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

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

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

で、また４章に戻ってきた。
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