haskell - 用于经典命题逻辑的 Quine 算法的 Prolog 实现(在 Quine 的 "Methods of Logic"中)

Question

我只知道一个证明者可以翻译 Quine 在他的《逻辑方法》一书中为经典命题逻辑提供的算法(哈佛大学出版社，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, xfy, '|').   % disjunction
:- op(1110, xfy, =>).    % conditional
:- op(1120, xfy, <=>).   % biconditional

真值常数是 top和 bot分别为真假。算法开始如下:对于任何命题公式 女 , 复制两份并替换 中出现次数最多的原子女 通过 top在第一个副本中，并由 bot在第二个副本中，然后对每个副本尽可能多地应用以下十个缩减规则:

 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

当然，对于否定和双重否定，我们也有以下规则:

 1. ~bot --> top
 2. ~top --> bot
 3. ~~p  --> p 

当没有 top也不是 bot在公式中，因此没有任何规则适用，再次拆分并选择一个原子将其替换为 top和 bot在另一张双面 table 上。公式 女 证明当且仅当算法以 top 结束时在所有副本中，并且无法证明，否则。
例子:

                         (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 编辑
这是双倍 posted在 SWI-Prolog 论坛上进行了热烈的讨论，证明 Prolog 已在此发布但未在此页面中复制。

Answer 1

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),
    dif(Variable, 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 之后插入一个切口。呼吁 promise 一个单一的选择。
现在实际更换一个 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, Replacement, Formula, Replaced) :-
    Formula =.. [Operator | Args],
    Args = [_ | _],
    maplist(variable_replacement_formula_replaced(Variable, Replacement), Args, ReplacedArgs),
    Replaced =.. [Operator | ReplacedArgs].

最后是证明者，构建一个类似 Haskell 版本的证明项:

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枚举变量的出现。可以根据自己的要求以各种方式使其更具确定性。
编辑: formula_simple的上述实现幼稚且低效:每次在公式的根部成功简化时，它都会重新审视所有子公式。但是在这个问题上，当根被简化时，子公式的新的简化将成为可能。这是一个新版本，它更加小心地首先完全重写子公式，然后只在根处迭代重写:

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指出这一点。重写规则必须扩展一点:

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).
...

有了这个，证明者表现得很好。