用于经典命题逻辑的 Quine 算法的 Prolog 实现(在 Quine 的“逻辑方法"中) [英] Prolog implementation of Quine's algorithm for classical propositional logic (in Quine's "Methods of Logic")
问题描述
我只知道一个证明者可以翻译 Quine 在他的著作 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
Truth 常量是 top 和 bot，分别代表 true 和 false.算法开始如下:对于任何命题公式F，将其复制两份，并将F中出现次数最多的原子替换为top 在第一个副本中，和由 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 --> top
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 and by bot 在另一个双面表格中.公式F被证明当且仅当算法在所有副本中都以top结尾，否则证明失败.
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.)
一、单一化简步骤:
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屋！
