问题描述
我只知道一个证明者,可以证明奎因在他的《逻辑方法》中为经典命题逻辑给出的算法(哈佛大学出版社,1982年,第1秒,第5页,第33- 40),这个证明者在Haskell,在这里: Quine's algorithm in Haskell
我尝试在Prolog中翻译Quine的算法,但是直到现在我还没有成功。很遗憾,因为它是一种有效的算法,Prolog的翻译很有趣。我将描述这个算法。一开始我唯一给出的Prolog代码是对测试证明者有用的运算符列表:
% operator deFinitions (TPTP Syntax)
:- op( 500,fy,~). % negation
:- op(1000,xfy,&). % conjunction
:- op(1100,'|'). % disjunction
:- op(1110,=>). % conditional
:- op(1120,<=>). % biconditional
对于 true 和 false ,真常量分别为top
和bot
。该算法开始如下:对于任何命题公式 F ,制作两个副本并将其在 F 中出现最高的原子替换为top
,第一个副本,在第二个副本中用bot
进行和,然后对每个副本应用以下十个归约规则,一次一次地对每个副本执行尽可能多的次数:>
1. p & bot --> bot
2. p & top --> p
3. p | bot --> p
4. p | top --> p
5. p => bot --> ~p
6. p => top --> top
7. bot => p --> top
8. top => p --> p
9. p <=> bot --> ~p
10. p <=> top --> p
当然,我们还有以下关于否定和双重否定的规则:
1. ~bot --> top
2. ~top --> bot
3. ~~p --> p
当公式中既没有top
也没有bot
时,则都不适用任何规则,请再次拆分并选择一个原子以top
代替 by bot
在另一个双面桌上。仅当该算法在所有副本中均以top
结尾并且未能得到证明时,证明公式 F 。
示例:
(p => q) <=> (~q => ~p)
(p => top) <=> (bot => ~p) (p => bot) <=> (top => ~p)
top <=> top ~p <=> ~p
top top <=> top bot <=> bot
top top
很明显,Quine的算法是对真值表方法的优化,但是从真值表生成器的程序代码开始,我没有成功地在Prolog代码中得到它。
欢迎至少开始提供帮助。预先,非常感谢。
Guy Coder编辑
这是SWI-Prolog论坛上的双重posted,该论坛进行了热烈的讨论,Prolog在哪里发布,但在此页面上未复制。
解决方法
Haskell代码对我来说似乎很复杂。这是基于问题中给出的算法描述的实现。 (使用SWI-Prolog库中的maplist
和dif
,但很容易实现。)
首先,一个简单的步骤:
formula_simpler(_P & bot,bot).
formula_simpler(P & top,P).
formula_simpler(P '|' bot,P).
formula_simpler(_P '|' top,top). % not P as in the question
formula_simpler(P => bot,~P).
formula_simpler(_P => top,top).
formula_simpler(bot => _P,top).
formula_simpler(top => P,P).
formula_simpler(P <=> bot,~P).
formula_simpler(P <=> top,P).
formula_simpler(~bot,top).
formula_simpler(~top,bot).
formula_simpler(~(~P),P).
然后,将这些步骤重复应用于子项并从根本上迭代,直到不再更改为止:
formula_simple(Formula,Simple) :-
Formula =.. [Operator | Args],maplist(formula_simple,Args,SimpleArgs),SimplerFormula =.. [Operator | SimpleArgs],( formula_simpler(SimplerFormula,EvenSimplerFormula)
-> formula_simple(EvenSimplerFormula,Simple)
; Simple = SimplerFormula ).
例如:
?- formula_simple(~ ~ ~ ~ ~ a,Simple).
Simple = ~a.
要用其他值替换变量,首先要在公式中查找变量的谓词:
formula_variable(Variable,Variable) :-
atom(Variable),dif(Variable,top),bot).
formula_variable(Formula,Variable) :-
Formula =.. [_Operator | Args],member(Arg,Args),formula_variable(Arg,Variable).
回溯时,它将枚举公式中变量的所有出现次数,例如:
?- formula_variable((p => q) <=> (~q => ~p),Var).
Var = p ;
Var = q ;
Var = q ;
Var = p ;
false.
这是下面的证明过程中唯一的不确定性来源,您可以在formula_variable
调用后插入剪切以提交给单个选择。
现在将Variable
中的Formula
实际替换为Replacement
:
variable_replacement_formula_replaced(Variable,Replacement,Variable,Replacement).
variable_replacement_formula_replaced(Variable,_Replacement,Formula,Formula) :-
atom(Formula),dif(Formula,Variable).
variable_replacement_formula_replaced(Variable,Replaced) :-
Formula =.. [Operator | Args],Args = [_ | _],maplist(variable_replacement_formula_replaced(Variable,Replacement),ReplacedArgs),Replaced =.. [Operator | ReplacedArgs].
最后是证明者,构造了类似于Haskell版本的证明术语:
formula_proof(Formula,trivial(Formula)) :-
formula_simple(Formula,top).
formula_proof(Formula,split(Formula,TopProof,BotProof)) :-
formula_simple(Formula,SimpleFormula),formula_variable(SimpleFormula,Variable),variable_replacement_formula_replaced(Variable,top,TopFormula),bot,BotFormula),formula_proof(TopFormula,TopProof),formula_proof(BotFormula,BotProof).
问题示例的证明:
?- formula_proof((p => q) <=> (~q => ~p),Proof).
Proof = split((p=>q<=> ~q=> ~p),p,split((top=>q<=> ~q=> ~top),q,trivial((top=>top<=> ~top=> ~top)),trivial((top=>bot<=> ~bot=> ~top))),trivial((bot=>q<=> ~q=> ~bot))) .
所有证明:
?- formula_proof((p => q) <=> (~q => ~p),trivial((bot=>q<=> ~q=> ~bot))) ;
Proof = split((p=>q<=> ~q=> ~p),trivial((p=>top<=> ~top=> ~p)),split((p=>bot<=> ~bot=> ~p),trivial((top=>bot<=> ~bot=> ~top)),trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p),trivial((bot=>q<=> ~q=> ~bot))) ;
false.
这包含很多冗余。同样,这是因为formula_variable
枚举了变量的出现次数。可以根据自己的需求以各种方式使它更具确定性。
编辑:formula_simple
的上述实现是幼稚且效率低下的:每次成功简化公式的根源时,它也会重新访问所有子公式。但是在这个问题上,当简化根时,子公式的新简化将变得不可能。这是一个新版本,在首先完全重写子公式,然后仅在根目录处迭代重写之前,要格外小心:
formula_simple2(Formula,maplist(formula_simple2,formula_rootsimple(SimplerFormula,Simple).
formula_rootsimple(Formula,Simple) :-
( formula_simpler(Formula,Simpler)
-> formula_rootsimple(Simpler,Simple)
; Simple = Formula ).
这快得多:
?- time(formula_simple(~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~(a & b & c & d & e & f & g & h & i & j & k & l & m & n & o & p & q & r & s & t & u & v & w & x & y & z),Simple)).
% 11,388 inferences,0.004 CPU in 0.004 seconds (100% CPU,2676814 Lips)
Simple = ~ (a&b&c&d&e&f&g&h& ... & ...).
?- time(formula_simple2(~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~(a & b & c & d & e & f & g & h & i & j & k & l & m & n & o & p & q & r & s & t & u & v & w & x & y & z),Simple)).
% 988 inferences,0.000 CPU in 0.000 seconds (100% CPU,2274642 Lips)
Simple = ~ (a&b&c&d&e&f&g&h& ... & ...).
编辑:如评论中所指出的那样,对于稍大的公式,上面编写的证明者可能会非常缓慢。问题是我忘记了一些运算符是可交换的!感谢jnmonette指出这一点。重写规则必须扩展一点:
formula_simpler(_P & bot,bot).
formula_simpler(bot & _P,P).
formula_simpler(top & P,P).
formula_simpler(bot '|' P,P).
...
并且证明者表现得很好。
,这是解决方案的框架。我希望它可以帮助您填补空缺。
is_valid(Formula) :-
\+ derive(Formula,bot).
is_satisfiable(Formula) :-
derive(Formula,top).
derive(bot,D):-
!,D=bot.
derive(top,D=top.
derive(Formula,D):-
reduce(Formula,Formula1),(
Formula=Formula1
->
branch(Formula1,D)
;
derive(Formula1,D)
).
现在,您需要实施reduce / 2(应用归约规则)(在子公式中递归),以及branch / 2(以不确定性将top或bot替换公式的原子),然后递归调用/ 2。像这样:
branch(Formula,D):-
pickAtom(Formula,Atom),(
Rep=top
;
Rep=bot
),replace(Formula,Atom,Rep,derive(Formula1,D).
,
似乎这种蛮力方法较旧(*),并且 由于Prolog代码非常小,因此甚至适合 裤子的口袋:
这是一个完整的实现。仅用于切割 优先进行重写,并且几乎对应 Haskell规则。除了Haskell可能没有 数据类型逻辑变量,例如Prolog:
:- op(300,fy,~).
eval(A,A) :- var(A),!.
eval(A+B,R) :- !,eval(A,X),eval(B,Y),simp(X+Y,R).
eval(A*B,simp(X*Y,R).
eval(~A,simp(~X,R).
eval(A,A).
simp(A,!.
simp(A+B,B) :- A == 0,A) :- B == 0,!.
simp(A+_,1) :- A == 1,!.
simp(_+B,1) :- B == 1,!.
simp(A*_,0) :- A == 0,!.
simp(_*B,0) :- B == 0,!.
simp(A*B,B) :- A == 1,A) :- B == 1,!.
simp(~A,1) :- A == 0,0) :- A == 1,!.
simp(A,A).
代码不是纯Prolog,并且使用非逻辑var / 1,(==)/ 2等。meta编程。像Boole一样,我们线性地减少并执行两个替换的加法运算,因此我们进行了Quine拆分而没有任何分支,并且通过单个前锋进行了处理:
judge(A,[B|R]) :- eval(A,B),term_variables(B,L),judge(B,L,R).
judge(_,[],R = [].
judge(A,[B|L],R) :-
copy_term(A-[B|L],C-[0|L]),copy_term(A-[B|L],D-[1|L]),judge(C*D,R).
在上面,我们使用copy_term / 2进行替换。这个想法是从Ulrich Neumerkels lambda库中借用的。我们还需要在eval / 2和simp / 2中使= here。这是您喜欢的任何ISO Prolog中运行的示例:
?- judge(A+ ~A,L).
L = [A+ ~A,1] /* Ends in 1,Tautology */
?- judge(A+ ~B,L).
L = [A+ ~B,~B,0] /* Ends in 0,Falsifiable */
?- judge(((P+Q)=<R)=:=((P=<R)*(Q=<R)),L).
L = [(P+Q =< R) =:= (P =< R)*(Q =< R),((Q =< R) =:= (Q =< R))*(R =:= R*(Q =< R)),(R =:= R)*((R =:= R)*(R =:= R*R)),1].
(*)来自:
U. Martin和T. Nipkow。布尔统一-到目前为止的故事。
在“统一”中,第437-455页。学术出版社,伦敦,1990年。