고전 명제 논리에 대한 Quine 알고리즘의 프롤로그 구현 (Quine의 "Methods of Logic"에서)

Aug 20 2020

나는 Quine이 그의 책 Methods of Logic (Harvard University Press, 1982, ch. 1 sec. 5, pp. 33-40) 에서 고전 명제 논리에 대해 제시 한 알고리즘을 번역하는 단 한 명의 증명자를 알고 있습니다.이 증명자는 Haskell에 있습니다. 현재 위치 : Haskell의 Quine 알고리즘

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

진실 상수는 topbot에 대한 각각 진실거짓 . 알고리즘의 시작은 다음과 같이 모든 명제 화학식 들어 F는 그것의 두 복사본을 만들고에서 가장 발생 갖는 원자로 대체 F를 하여 top제 복사하여, 에서 bot두번째 카피하고 다음 열 감소는 하나의 규칙 적용 각 사본에 대해 가능한 한 여러 번 규칙을 지정하십시오.

 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 

둘 다 존재하지 않는 경우 topbot규칙 중 어느 것도 적용되지 않도록 수식이를 다시 분할하여 대체 이상의 원자를 선택 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 코드로 가져 오지 못했습니다.

최소한 시작하는 데 도움이 될 것입니다. 미리 감사드립니다.


Guy Coder 편집

이것은 활발한 토론이 있고 Prolog Prolog가 게시되었지만이 페이지에서 재현되지 않는 SWI-Prolog 포럼에 이중 게시 되었습니다.

답변

6 IsabelleNewbie Aug 27 2020 at 04:02

Haskell 코드는 나에게 복잡해 보였습니다. 다음은 질문에 제공된 알고리즘의 설명을 기반으로 한 구현입니다. (사용 maplistdif에서 SWI - 프롤로그 라이브러리,하지만 쉽게에 자체 포함.)

첫째, 단일 단순화 단계 :

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의 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으로 대체하는 branch / 2를 구현 한 다음 재귀 적으로 derive / 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).

코드는 순수한 프롤로그가 아니며 비논리적 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 프롤로그에서 실행되는 예제입니다.

?- 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 페이지. Academic Press, 런던, 1990.