はじめに
一度ちゃんと論理学の本を読みたいと思うのですが、なかなか難しいです。
せめて、Prolog (SWI-Prolog) で命題論理を解けるようになりたいと思いました。
与えられた論理式について、ルールに従って書き換えていって簡約化していく、これ以上簡約化できないところまで来たらそれが答えである、という方針で考えることにします。
与えられた論理式をルールに従って書き換えて簡約化していく、という方針は「項書換えシステム（Term Rewriting System, TRS）」として知られています。
というわけで、いろいろ調べたり試行錯誤したりして、こんな表示ができるプログラムを作成しました（その他実行例は github 参照）。
?- trs_resolve([ (a ∨ b ∨ c) ∧ (¬a ∨ b) ∧ (¬b ∨ c) ∧ (¬c) ], Result).
a∨b∨c∧(¬a∨b)∧(¬b∨c)∧ ¬c
---------------- 論理積の消去_conjunction_elimination ( [a∨b∨c∧(¬a∨b)∧(¬b∨c)∧ ¬c] ⊢ [assume(a∨b∨c∧(¬a∨b)∧(¬b∨c)),assume(¬c)] )
¬c, a∨b∨c∧(¬a∨b)∧(¬b∨c)
---------------- 論理積の消去_conjunction_elimination ( [a∨b∨c∧(¬a∨b)∧(¬b∨c)] ⊢ [assume(a∨b∨c∧(¬a∨b)),assume(¬b∨c)] )
¬c, a∨b∨c∧(¬a∨b), ¬b∨c
---------------- 選言三段論法_disjunctive_syllogism2 ( [¬c] \ [¬b∨c] ⊢ [assume(¬b)] )
¬b, ¬c, a∨b∨c∧(¬a∨b)
---------------- 論理積の消去_conjunction_elimination ( [a∨b∨c∧(¬a∨b)] ⊢ [assume(a∨b∨c),assume(¬a∨b)] )
¬b, ¬c, ¬a∨b, a∨b∨c
---------------- 選言三段論法_disjunctive_syllogism2 ( [¬b] \ [¬a∨b] ⊢ [assume(¬a)] )
¬a, ¬b, ¬c, a∨b∨c
---------------- 選言三段論法_disjunctive_syllogism2 ( [¬c] \ [a∨b∨c] ⊢ [assume(a∨b)] )
¬a, ¬b, ¬c, a∨b
---------------- 選言三段論法_disjunctive_syllogism ( [¬a] \ [a∨b] ⊢ [assume(b)] )
assume(b), ¬a, ¬b, ¬c
---------------- 矛盾律_contradiction ( [assume(b),¬b] ⊢ [⊥(b)] )
¬a, ¬c, ⊥(b)
Result = [⊥] .
?-
ここで、
-
assume(P)は「P を仮定として扱う」 -
⊢は「導出される」を表す記号
として表示しています。
項を書き換えるルールを設定ファイルに書くことにして、その記述フォーマットはどういう形がよいだろう、と調べているうちに、CHR (Constraint Handling Rules) に行き当たりました。
Constraint Handling Rules とその記述方法
CHR では制約ストアに格納された論理式の集合を扱います。
CHR は「制約ストア（制約の集合）」に対して、ルールに従って制約を追加・削除することで状態を変化させる言語です。
簡略化ルール
h1, h2,...,hn <=> g1,g2,...,gm|b1,b2,...,bo.
制約ストア上に頭部 h1,h2,...,hn に該当する論理式が存在して、ガード条件 g1,g2,...,gm を満たすとき、制約ストアにある頭部に該当する論理式を b1,b2,...,bo` に書き換えます。
h1, h2,...,hi \ hj,...hn <=> g1,g2,...,gm|b1,b2,...,bo.
のように頭部が \ で区切られているならば \ より前に記述された部分は制約ストアに残したままにして \ より後ろに記述された部分のみ b1,b2,...,bo` に書き換えます。
伝播ルール
h1, h2,...,hn ==> g1,g2,...,gm|b1,b2,...,bo.
制約ストア上に頭部 h1,h2,...,hn に該当する論理式が存在して、ガード条件 g1,g2,...,gm を満たすとき、b1,b2,...,bo` を制約ストアに追加します。
ルール名
いずれのルールにおいても、先頭に 名前 @ を追加することでルール名をつけることができます。
記述例
三段論法（P → Q かつ Q → R ならば P → R である、ということ）を
(P → Q), (Q → R) <=> (P → R).
というルールで記述できます。但し、→/2 は予め CHR で制約を表現するのに用いるものだということを宣言しておく必要があります。
例えばこんな感じです:
:- op(900, xfy, '→').
:- chr_constraint (→)/2.
モーダスポネンス（前件肯定）
{\displaystyle \qquad {\frac {(P\rightarrow Q),P}{Q}}}
（P → Q と P があるならば、それらを Q に書き換える）は
P → Q, assume(P) <=> assume(Q).
のように書くことができます。assume/1 は
:- chr_constraint assume/1.
のように定義しておいた制約です。assume(P) なんて使わず素直に P と書けば
P → Q, P <=> Q.
とすっきりした見た目になるのですが、残念ながらこのような書き方はできません。
CHR では、任意の項（例えば単なる P）を直接扱うことはできず、あらかじめ chr_constraint で宣言した述語のみが制約として利用可能です。
そのため、単なる論理式 P は assume(P) のようにラップして扱います。
かといって、いつまでも assume でラップされたままだと取り扱いが煩雑となるので、assume を使う必要がない場合に assume を外すルールが必要です。
unwrap @ assume(P) <=> compound(P) | P.
とすることで、assume(P) において「P が複合項である」＝「P が既になんらかの制約として表現されている」場合には assume を外します。
...と、こんな感じで考えながら項書換えルールを書いていきます。
CHR で解く命題論理
こうやって CHR に合わせてルールを記述していくと、自分が書いていた項書換えプログラムと CHR と双方で同じルールを動かして答え合わせができます。
CHR バージョンは以下です（github）:
:- use_module(library(chr)).
:- op(1000, xfy, '⊢').
:- op(900, xfy, '→').
:- op(900, xfy, '⇔').
:- op(550, yfx, '∨').
:- op(550, yfx, '∧').
:- op(150, fy, '¬').
:- chr_constraint (⊥)/1.
:- chr_constraint (→)/2.
:- chr_constraint (∨)/2.
:- chr_constraint (∧)/2.
:- chr_constraint (¬)/1.
:- chr_constraint assume/1.
ド_モルガンの法則_de_morgan_law @ ¬(P ∨ Q) <=> ¬ P ∧ ¬ Q.
ド_モルガンの法則_de_morgan_law @ ¬(P ∧ Q) <=> ¬ P ∨ ¬ Q.
unwrap @ assume(P) <=> compound(P) | P.
分配 @
P ∨ (Q ∧ R) <=> \+ P = Q | P ∨ Q, P ∨ R.
吸収 @
P ∨ (P ∧ _) <=> assume(P).
'前件肯定_modus_ponens' @
assume(P), (P → Q) <=> assume(Q).
後件否定_modus_tollens @
¬ Q \ (P → Q) <=> ¬ P.
否定導入_not @
P → ⊥ <=> ¬ P.
否定導入_not @
P → ⊥(_) <=> ¬ P.
二重否定の除去_double_negative_elimination @
¬ ¬ P <=> assume(P).
選言三段論法_disjunctive_syllogism @
¬ P \ (P ∨ Q) <=> assume(Q).
選言三段論法_disjunctive_syllogism2 @
¬ P \ (Q ∨ P) <=> assume(Q).
仮言三段論法_hypothetical_syllogism @
(P → Q), (Q → R) <=> (P → R).
論理和の消去_disjunction_elimination @
(P → Q), (R → Q), (P ∨ R) <=> assume(Q).
論理和の消去_disjunction_elimination @
(P ∨ P) <=> assume(P).
論理積の消去_conjunction_elimination @
(P ∧ Q) <=> assume(P), assume(Q).
論理積の消去_conjunction_elimination @
assume(P), assume(P) <=> assume(P).
矛盾律_contradiction @
assume(A), ¬ A <=> ⊥(A).
導出_resolution @
L ∨ P, ¬ L ∨ Q <=>
L \= P, L \= ¬ P, ¬ L \= P, L \= Q, L \= ¬ Q, ¬ L \= Q |
P ∨ Q.
エンジン部分は CHR ライブラリとして用意されているものを使うだけなので、ルールを並べるだけです。
この内容で、sample_chr.pl というファイルを作り、swipl を起動して、[sample_chr] を投入すると（consult('sample_chr.pl') でもよい）:
?- [sample_chr].
true.
?-
この状態で、クエリとして制約を投入すると、適用可能なルールが自動的に適用され、最終的な制約ストアの状態が表示されます。
例えば、三段論法の場合は、以下のようにクエリ「A → B, B → C.」を投入すると「A→C」を返してくれます:
?- A → B, B → C.
A→C.
もっと複雑な式についても、例えば:
?- (P ∨ Q) ∧ (¬ P ∨ Q) ∧ (P ∨ ¬ Q) ∧ (¬ P ∨ ¬ Q).
⊥(Q).
となって、自分が作った項書換えプログラムの結果が正しいことが確認できました。
CHR で項書換えの履歴を表示できれば完璧なのですが、多分デバッガで見ていくくらいしかないのではないかと思います。
結び
- Prolog で項書換えシステムを実装しました。
- 命題論理の推論を「書き換え」として扱うことで、実装と挙動の理解がしやすくなりました。
- さらに CHR で同じルールを記述することで、自作エンジンの正しさを検証できました。
制約処理系として知られている CHR は「書き換え規則を直接実行できる言語」として見ると、非常に強力であることがわかりました。