古典的な命題論理のためのQuineのアルゴリズムのProlog実装（Quineの「論理の方法」）

Aug 20 2020

Quineが彼の著書Methodsof Logic（Harvard University Press、1982、ch。1sec。5、pp。33-40）で古典的な命題論理に与えたアルゴリズムを翻訳する証明者は、私だけが知っています。この証明者はHaskellにいます。ここにあります：HaskellのQuineのアルゴリズム

QuineのアルゴリズムをPrologで翻訳しようとしましたが、今まで成功しませんでした。それは効率的なアルゴリズムであり、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するために、それぞれ、真と偽。アルゴリズムの開始を次のように任意の命題式の場合はF、それの2つのコピーを作成し、で最高の発生がある原子置き換えるFをすることによってtop最初のコピーでは、とによってbot第二のコピーでをし、次の10削減は1ルール適用コピーごとに、できるだけ多くの回数を一度にルール化します。

 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 とによって、botさらに別の両面のテーブルに。式Fは、アルゴリズムが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コードでそれを取得することに成功しませんでした。

少なくとも始めるための助けは大歓迎です。よろしくお願いします。

GuyCoderによる編集

これは、活発な議論があり、証明者Prologが公開されているが、このページでは複製されていないSWI-Prologフォーラムに二重に投稿されています。

回答

6 IsabelleNewbie Aug 27 2020 at 04:02

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呼び出しの後にカットを挿入して、単一の選択にコミットすることができます。

今、実際の交換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).
...

そしてこれで証明者はうまく振る舞います。

3 jnmonette Aug 21 2020 at 00:47

これがソリューションの骨組みです。それがあなたが穴を埋めるのを助けることができることを願っています。

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のいずれかに置き換え、再帰的にderive / 2を呼び出すbranch / 2を実装する必要があります。何かのようなもの：

branch(Formula, D):-
    pickAtom(Formula, Atom),
    (
      Rep=top
    ; 
      Rep=bot
    ),
    replace(Formula, Atom, Rep, Formula1),
    derive(Formula1,D).

3 MostowskiCollapse Aug 27 2020 at 01:18

このブルートフォース方式は古いようです（*）。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, 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などを使用します。メタプログラミング。ブールのように、2つの置換を線形に減らして接続詞を実行するので、分岐せずに単一のフロントを介してクワイン分割を実行します。

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を使用して置換を行います。このアイデアは、UlrichNeumerkelsラムダライブラリから借用しています。また、eval / 2とsimp / 2で= <と=：=を利用できるようにする必要があります。完全なソースコードについては、こちらをご覧ください。これは、お気に入りのISOPrologで実行される例です。

?- 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。マーティンとT.ニプコウ。ブール統合—これまでの話。
統一、437〜455ページ。アカデミックプレス、ロンドン、1990年。