经典命题逻辑的Quine算法的Prolog实现(在Quine的“逻辑方法"中) [英] Prolog implementation of Quine's algorithm for classical propositional logic (in Quine's "Methods of Logic")
问题描述
我只知道一个证明者，可以证明奎因在他的《逻辑方法》中为经典命题逻辑给出的算法(哈佛大学出版社，1982年，第1秒，第5页，第33- 40)，这个证明者在Haskell，在这里: Haskell中的Quine算法
I know only one prover that translates the algorithm that Quine gave for classical propositional logic in his book Methods of Logic (Harvard University Press, 1982, ch. 1 sec. 5, pp. 33-40), this prover is in Haskell and it is here: Quine's algorithm in Haskell
我尝试在Prolog中翻译Quine的算法，但是直到现在我还没有成功.很遗憾，因为它是一种有效的算法，Prolog的翻译很有趣.我将描述这个算法.我一开始唯一给出的Prolog代码是对测试证明者有用的运算符列表:
I tried to translate Quine's algorithm in Prolog, but until now I have not succeeded. It is a pity because it is an efficient algorithm and a Prolog translation would be interesting. I am going to describe this algorithm. The only Prolog code that I give at the start is the list of operators that would be useful to test the prover:
% operator definitions (TPTP syntax)
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
对于 true 和 false ，
真常量分别为top和bot.该算法开始如下:对于任何命题公式 F ，制作两个副本并将第一副本中top替换为在 F 中发生率最高的原子. ，然后在第二个副本中按bot依次和，然后针对每个副本，一次应用以下十条归约规则，并尽可能多地一次应用一个规则:
Truth constants are top and bot for, respectively, true and false. The algorithm starts as follows: For any propositional formula F, make two copies of it and replace the atom which has the highest occurrence in F by top in the first copy, and by bot in the second copy, and then apply the following ten reduction rules one rule at a time for as many times as possible, for each of the copies:
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
当然，我们还有以下关于否定和双重否定的规则:
Of course, we have also the following rules for negation and double negation:
1. ~bot --> top
2. ~top --> bot
3. ~~p --> p
当公式中既没有top也没有bot时，则都不适用任何规则，请再次拆分并选择一个原子以将其替换为top ，并将替换为bot在另一张双面桌子上.且仅当算法在所有副本中均以top结尾且未能通过证明时，方可证明公式 F .
When there is neither top nor bot in the formula so none of the rules apply, split it again and pick one atom to replace it by top and by bot in yet another two sided table. The formula F is proved if and only if the algorithm ends with top in all copies, and fails to be proved, otherwise.
示例:
(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代码中得到它.
It is clear that Quine's algorithm is an optimization of the truth tables method, but starting from codes of program of truth tables generator, I did not succeed to get it in Prolog code.
欢迎至少开始提供帮助.预先，非常感谢.
A help at least to start would be welcome. In advance, many thanks.
Guy Coder的编辑
这是两次发表 SWI-Prolog论坛，进行了热烈的讨论，Prolog在哪里发布，但在本页面中未复制.
This is double posted at SWI-Prolog forum which has a lively discussion and where provers Prolog are published but not reproduced in this page.
推荐答案
Haskell代码对我来说似乎很复杂.这是基于问题中给出的算法描述的实现. (使用SWI-Prolog库中的maplist和dif，但易于实现.)
The Haskell code seemed complicated to me. Here's an implementation based on the description of the algorithm given in the question. (Using maplist and dif from the SWI-Prolog library, but easy to make self-contained.)
首先，一个简单的步骤:
First, single simplification steps:
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).
然后，将这些步骤重复应用于子项并从根本上迭代，直到不再更改为止:
Then, iterated application of these steps to subterms and iteration at the root until nothing changes anymore:
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.
要用其他值替换变量，首先要在公式中查找变量的谓词:
For the replacement of variables by other values, first a predicate for finding variables in formulas:
formula_variable(Variable, Variable) :-
atom(Variable),
dif(Variable, top),
dif(Variable, bot).
formula_variable(Formula, Variable) :-
Formula =.. [_Operator | Args],
member(Arg, Args),
formula_variable(Arg, Variable).
回溯时，它将枚举公式中变量的所有出现次数，例如:
On backtracking this will enumerate all occurrences of variables in a formula, for example:
?- formula_variable((p => q) <=> (~q => ~p), Var).
Var = p ;
Var = q ;
Var = q ;
Var = p ;
false.
这是下面的证明过程中唯一的不确定性来源，您可以在formula_variable调用后插入剪切以提交给单个选择.
This is the only source of nondeterminism in the proof procedure below, and you can insert a cut after the formula_variable call to commit to a single choice.
现在将Formula中的Variable实际替换为Replacement:
Now the actual replacement of a Variable in a Formula by 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, Replacement, Formula, Replaced) :-
Formula =.. [Operator | Args],
Args = [_ | _],
maplist(variable_replacement_formula_replaced(Variable, Replacement), Args, ReplacedArgs),
Replaced =.. [Operator | ReplacedArgs].
最后是证明者，构造了类似于Haskell版本的证明术语:
And finally the prover, constructing a proof term like the Haskell version:
formula_proof(Formula, trivial(Formula)) :-
formula_simple(Formula, top).
formula_proof(Formula, split(Formula, Variable, TopProof, BotProof)) :-
formula_simple(Formula, SimpleFormula),
formula_variable(SimpleFormula, Variable),
variable_replacement_formula_replaced(Variable, top, Formula, TopFormula),
variable_replacement_formula_replaced(Variable, bot, Formula, 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), 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))) ;
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))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
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))) ;
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))) ;
false.
这包含很多冗余.同样，这是因为formula_variable枚举了变量的出现次数.可以根据自己的需求以各种方式使它更具确定性.
This contains lots of redundancy. Again, this is because formula_variable enumerates occurrences of variables. It can be made more deterministic in various ways depending on one's requirements.
编辑:formula_simple的上述实现是幼稚且低效的:每次成功简化公式的根源时，它也会重新访问所有子公式.但是在这个问题上，当简化根时，子公式的新简化将变得不可能.这是一个新版本，在首先完全重写子公式，然后仅在根目录处迭代重写之前，要格外小心:
The above implementation of formula_simple is naive and inefficient: Every time it makes a successful simplification at the root of the formula, it revisits all of the subformulas as well. But on this problem, no new simplifications of the subformulas will become possible when the root is simplified. Here is a new version that is more careful to first fully rewrite the subformulas, and then only iterate rewrites at the root:
formula_simple2(Formula, Simple) :-
Formula =.. [Operator | Args],
maplist(formula_simple2, Args, SimpleArgs),
SimplerFormula =.. [Operator | SimpleArgs],
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 指出这一点.重写规则必须扩展一点:
As pointed out in the comments, the prover as written above can be veeery slow on slightly bigger formulas. The problem is that I forgot that some operators are commutative! Thanks jnmonette for pointing this out. The rewrite rules must be expanded a bit:
formula_simpler(_P & bot, bot).
formula_simpler(bot & _P, bot).
formula_simpler(P & top, P).
formula_simpler(top & P, P).
formula_simpler(P '|' bot, P).
formula_simpler(bot '|' P, P).
...
并且证明者表现得很好.
And with this the prover behaves nicely.
这篇关于经典命题逻辑的Quine算法的Prolog实现(在Quine的“逻辑方法"中)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
