発端
自動定理証明のことを読んだのは、後藤滋樹先生の「記号処理プログラミング」（岩波書店）でした。それはLispで書かれていて、考え方が説明されていました。これをPrologでやれたら面白いな、と始めたのが３～4年前だったと思います。当時はSchemeの拡張としてVM方式で動作するS式Prologを作っていました。そのテストの意味もあったように思います。この度、エジンバラPrologである自作O-Prolog処理系をテストするために、書き直しました。
動作の仕組み
証明は2段階から成ります。（１）連言標準形（conjunction normal form)に変換する。（２）その変換したものがトートロジーになっているかどうかを判定する。 トートロジーならその定理は正しいということになります。
金物表現
数理論理学の記号はパソコン上ではそのまま使えないので、BratkoのProlog本にあった例に従うこととします。
かつ ＆
または v
否定 ～
含意 =>
含意は私のオリジナルです。-> はISOPrologで組込み演算子として定義されているため、=>を使うこととしました。論理式は、数理論理学の本ではA,Bのように大文字のアルファベットを使うようなのですが、それですとPrologの変数と解釈されてしまいます。小文字のa,bなどをもって論理式とすることとしました。
独自演算子はop述語て定義することができます。
:- op(800,xfy,=>).
:- op(700,xfy,v).
:- op(600,xfy,&).
:- op(500,fy,~).
この結果、数理論理学と同様に、中置記法で自然に表現することができます。
例
a => b
~(a & b)
~a v ~ b
連言標準形 cnfの実装
連言標準形（conjunction normal form)は次の形式のものです。
(L11 v L12 v ... v l1m) & (L21 v L22 v ... L2n) & ... &(Lp1 v Lp2 V ...Lpr)
Lは論理式です。直観的にいうと「または」でひとくくりにして、それらを「かつ」でつないだものです。この形式にすると都合がいいのですが、そのことは後述します。
連言標準形（以下「cnf]）は、３つの変換ルールにより求めることができます。
（１）ドモルガンの法則
~(a & b) <===> ~a v ~ b
（２）二重否定の法則
~ ~ a <===> a
（３）分配律
(a & b) v (a & c) <===> a & (b v c)
含意は同等な論理式に置き換えます。
a => b <===> ~a v b
どうしてこうなるのかは、wikipediaのベン図をご覧ください。
https://ja.wikipedia.org/wiki/%E8%AB%96%E7%90%86%E5%8C%85%E5%90%AB
Prologのコードは次のようになります。
%論理式は記号アトムで表される
cnf(X,X) :- atomic(X).
%ドモルガンの法則
cnf(~(X & Y),Z) :- write('rule1 '),cnf(~X v ~Y,Z).
%二重否定の法則
cnf(~ ~ X,Z) :- write('rule2 '),cnf(X,Z).
%分配律
cnf((A & B) v (A & C),Z) :-
write('rule3 '),cnf(A & (B v C),Z).
%再帰構造
cnf(X & Y,X1 & Y1) :- write('rule4 '),cnf(X,X1),cnf(Y,Y1).
cnf(X v Y,X1 v Y1) :- write('rule5 '),cnf(X,X1),cnf(Y,Y1).
cnf(~ X,~ Z) :- write('rule6 '),cnf(X,Z).
%含意
cnf(X => Y,Z) :- write('rule7 '),cnf(~X v Y,Z).
cnfの動作テスト
うまくいくかテストしてみます。
O-Prolog Ver0.45
|
yes
| ?- cnf(~(a & ~(a & ~b)),X).
rule1 rule5 rule6 rule2 rule4 rule6 X = ~a v a&~b
yes
|
どの変換規則を使っているのかを表示するようにしています。だいじょうぶ（かな？）
トートロジー判定
論理式が定理として証明される場合には必ずトートロジーとなります。私の言葉だとどうも説明不足、誤解を生じそうですので、後藤滋樹先生の言葉をお借りすることにします。
「記号処理プログラミング」 後藤滋樹 著 岩波書店
さらに重要な性質として、ここに示した公理から導かれる定理はかならずトートロジーになること、逆に任意のトートロジーは必ず定理として証明できることがわかっている。そこで命題論理における定理の証明を次のように考えることができる。すなわち、「与えられた論理式が命題論理の定理になるか否かを判定するためには、その論理式がトートロジーになるか否かを計算すればよい」。
連言標準形に変形したのは、このトートロジー判定をやりやすくするためでした。トートロジーというのは常に真になる論理式のことです。カッコでくくられた「または」のくくりがトートロジーであるとは aと~aとを含む場合です。これを相補的というそうです。「かつ」で結ばれたそれぞれの「または」すべてがトートロジーであるならば、全体としてトートロジーであることが判定できます。
Prologのコードは以下のようです。
%トートロジー
tautology(X & Y) :- or_tautology(X),tautology(Y).
tautology(X) :- or_tautology(X).
%部分論理式の相補確認
or_tautology(X v Y) :- complement(~X,Y).
or_tautology(~X v Y) :- complement(X,Y).
%相補的
complement(X,X).
complement(X,X v _).
complement(X,Y v Ys) :- complement(X,Ys).
定理証明
さあ、ここまで出来上がれば定理証明はもうちょっとです。論理式を連言標準形に変換して、それがトートロジーになっているかどうかを判定すればいいだけです。
Prologコードは次のようになります。
proof(X) :- cnf(X,Y),tautology(Y).
うまくいくでしょうか。
a => a は直観で考えても正しいはずです。
| ?- proof(a=>a).
rule7 rule5 rule6 yes
| ?- proof(a=>b).
rule7 rule5 rule6 no
よさそうですね。 後藤先生の本にある例で試してみます。
| ?- proof(a=>b=>a).
rule7 rule5 rule6 rule7 rule5 rule6 yes
|
うまくいっているようです。
私は数理論理学の専門教育を受けているわけではありません。単なる好き者です。誤りがありましたら、ご指摘いただければ幸いです。
コード
最後に全コードを掲載します。
:- op(800,xfy,=>).
:- op(700,xfy,v).
:- op(600,xfy,&).
:- op(500,fy,~).
proof(X) :- cnf(X,Y),tautology(Y).
%論理式は記号アトムで表される
cnf(X,X) :- atomic(X).
%ドモルガンの法則
cnf(~(X & Y),Z) :- write('rule1 '),cnf(~X v ~Y,Z).
%二重否定の法則
cnf(~ ~ X,Z) :- write('rule2 '),cnf(X,Z).
%分配律
cnf((A & B) v (A & C),Z) :-
write('rule3 '),cnf(A & (B v C),Z).
%再帰構造
cnf(X & Y,X1 & Y1) :- write('rule4 '),cnf(X,X1),cnf(Y,Y1).
cnf(X v Y,X1 v Y1) :- write('rule5 '),cnf(X,X1),cnf(Y,Y1).
cnf(~ X,~ Z) :- write('rule6 '),cnf(X,Z).
%含意
cnf(X => Y,Z) :- write('rule7 '),cnf(~X v Y,Z).
%トートロジー
tautology(X & Y) :- or_tautology(X),tautology(Y).
tautology(X) :- or_tautology(X).
%部分論理式の相補確認
or_tautology(X v Y) :- complement(~X,Y).
or_tautology(~X v Y) :- complement(X,Y).
%相補的
complement(X,X).
complement(X,X v _).
complement(X,Y v Ys) :- complement(X,Ys).
参考文献
「記号処理プログラミング」 後藤滋樹 著 岩波書店
「数理論理学序説」 前原昭二 著 共立出版㈱