9

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

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

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.

Example:

                         (p => q) <=> (~q => ~p)

 (p => top) <=> (bot => ~p)                 (p => bot) <=> (top => ~p)

       top  <=>  top                              ~p   <=>  ~p  

            top                       top <=> top                bot <=> bot

                                          top                        top

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.

EDIT by Guy Coder

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.

4

3 回答 3

5

Haskell 代码对我来说似乎很复杂。这是基于问题中给出的算法描述的实现。（使用maplist和dif来自 SWI-Prolog 库，但易于实现自包含。）

一、单一化简步骤：

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调用后插入一个剪切来承诺一个单一的选择。

现在实际替换 a中的Variablea ：FormulaReplacement

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

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

于 2020-08-26T21:02:37.227 回答
3

警告！我们不使用 TPTP 语法，而是使用 SWI-Prolog CLP(B) 的语法。似乎这种蛮力方法较旧（*），并且由于 Prolog 代码如此之小，它甚至可以放在裤子的口袋里：

在此处输入图像描述

这是一个完整的实现。cut 仅用于优先重写，并且几乎对应于 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, R) :- !, eval(A, X), eval(B, Y), simp(X*Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).

simp(A, A) :- var(A), !.
simp(A+B, B) :- A == 0, !.
simp(A+B, 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, !.
simp(A*B, A) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).

该代码不是纯 Prolog 并使用非逻辑 var/1、(==)/2 等。元编程。像 Boole 一样，我们线性减少并执行两个替换的合取，因此我们在没有一些分支的情况下通过单个前端进行 Quine 拆分：

judge(A, [B|R]) :- eval(A, B), 
                   term_variables(B, L), judge(B, L, R).

judge(_, [], R) :- !, 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 中提供 =< 和 =:=。有关完整的源代码，请参见此处。以下是在您喜欢的任何 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 年。

于 2020-08-26T18:18:27.840 回答
3

这是解决方案的骨架。我希望它可以帮助你填补漏洞。

is_valid(Formula) :-
    \+ derive(Formula,bot).

is_satisfiable(Formula) :-
    derive(Formula, top).

derive(bot,D):-
    !,
    D=bot.
derive(top,D):-
    !,
    D=top.
derive(Formula,D):-
    reduce(Formula, Formula1),
    (
      Formula=Formula1
    ->
      branch(Formula1,D)
    ;
      derive(Formula1,D)
    ).

现在您需要实现应用归约规则的reduce/2（在子公式中递归），以及用top 或bot 不确定地替换公式的原子的branch/2，然后递归调用derive/2。就像是：

branch(Formula, D):-
    pickAtom(Formula, Atom),
    (
      Rep=top
    ; 
      Rep=bot
    ),
    replace(Formula, Atom, Rep, Formula1),
    derive(Formula1,D).
于 2020-08-20T17:47:26.433 回答