日々の流転

λ. SATCHMOで遊ぶ

先日の渕一博記念コロキウム『論理と推論技術：四半世紀の展開』での長谷川隆三氏の発表『モデル生成型定理証明系MGTPの要素技術』(スライド)で紹介されていたSATCHMOで少し遊んでみる。 これは節集合のモデルを作ることで、充足可能性を証明するのだとか。なので、当然、証明したい論理式の否定を与えてモデルが存在しないことを確認すれば、その論理式が恒真であることがわかるので、定理証明機として使うことが出来ると。

スライドで紹介されていたソースコードそのままだと SWI Prolog に怒られてしまったので、演算子の優先順位とあと動的に変化する述語をdynamicディレクティブで指示するようにしておく。

% satchmo.pl
:- op(1200, xfy, '--->').
:- dynamic false/0.

satisfiable :- is_violated(C), !, satisfy(C), satisfiable.
satisfiable.

is_violated(C) :- (A--->C), call(A), not(C).

satisfy(C) :- component(X,C), asserta(X),
              on_backtracking(retract(X)),
              not(false).

component(X,(Y;Z)) :- !, (X=Y; component(X,Z)).
component(X,X).

on_backtracking(_).
on_backtracking(X) :- call(X), !, fail.

しかし、トリッキーだなぁ。 Prologはこういうのが書けるのが楽しい。

問題S1

まずはスライドにあった問題S1。 Prologと同じで「,」がandで「;」がorを表している。

% s1.pl
:- dynamic p/1, q/1, r/1, s/1.

true ---> p(a); q(b).
q(X) ---> s(f(X)).
r(X) ---> s(X).
p(X) ---> q(X); r(X).
p(X), s(X) ---> false.
q(X), s(Y) ---> false.

で、satchmoを呼び出して充足可能性をチェック。

?- consult(satchmo).
Yes
?- consult(s1).
Yes
?- satisfiable.
No
?- 

うん、ちゃんと充足不可能なことを示してくれた。

モデルが存在する例

次はちゃんとモデルが存在する例を試してみる。

% hoge.pl
:- dynamic p/1, q/1.

true ---> p(x); q(x).
p(X) ---> false.
q(X) ---> q(X).

実行。

?- consult(satchmo).
Yes
?- consult(hoge).  
Yes
?- satisfiable.  
Yes

というわけで、充足可能なことが分かったので、今度はlistingを使ってPrologのデータベース中の述語を表示してモデルを調べてみる。

?- listing.
(略)
:- dynamic q/1.
q(x).
(略)

値域限定

色々と試していたら、satisfiableはNoになって欲しい節集合で、試したらYesになってしまったものがあって、どうしてなのか少し悩んでしまった。 原因は、SATCHMOの仮定している値域限定「節の結論部に現れる変数は仮定部にも現れなくてはならない」という制約に違反してしまっていたからだった。 なるほど、なるほど。