Implementazione prologo dell'algoritmo di Quine per la logica proposizionale classica (in "Metodi di logica" di Quine)
Conosco solo un prover che traduce l'algoritmo che Quine ha fornito per la logica proposizionale classica nel suo libro Methods of Logic (Harvard University Press, 1982, cap. 1 sec.5, pp. 33-40), questo prover è in Haskell e è qui: l'algoritmo di Quine in Haskell
Ho provato a tradurre l'algoritmo di Quine in Prolog, ma fino ad ora non ci sono riuscito. È un peccato perché è un algoritmo efficiente e una traduzione Prolog sarebbe interessante. Descriverò questo algoritmo. L'unico codice Prolog che fornisco all'inizio è l'elenco degli operatori che sarebbero utili per testare il 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
Le costanti di verità sono tope botper, rispettivamente, vero e falso . L'algoritmo inizia come segue: per ogni formula proposizionale F , creane due copie e sostituisci l'atomo che ha l'occorrenza più alta in F con topnella prima copia e con botnella seconda copia, quindi applica le seguenti dieci regole di riduzione una regola alla volta il maggior numero di volte possibile, per ciascuna delle copie:
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
Naturalmente, abbiamo anche le seguenti regole per la negazione e la doppia negazione:
1. ~bot --> top
2. ~top --> bot
3. ~~p --> p
Quando non v'è topné botla formula in modo nessuna delle regole diffusa, raggruppati nuovamente e scegliere un atomo di sostituirli con top e da botin ancora un'altra tabella bifacciale. La formula F è dimostrata se e solo se l'algoritmo termina con topin tutte le copie, e non può essere dimostrata, altrimenti.
Esempio:
(p => q) <=> (~q => ~p)
(p => top) <=> (bot => ~p) (p => bot) <=> (top => ~p)
top <=> top ~p <=> ~p
top top <=> top bot <=> bot
top top
È chiaro che l'algoritmo di Quine è un'ottimizzazione del metodo delle tabelle di verità, ma partendo da codici di programma di generatore di tabelle di verità, non sono riuscito a ottenerlo in codice Prolog.
Un aiuto almeno per iniziare sarebbe gradito. In anticipo, molte grazie.
EDIT di Guy Coder
Questo è pubblicato due volte sul forum SWI-Prolog che ha una vivace discussione e dove i prover Prolog sono pubblicati ma non riprodotti in questa pagina.
Risposte
Il codice Haskell mi sembrava complicato. Ecco un'implementazione basata sulla descrizione dell'algoritmo fornita nella domanda. (Utilizzando mapliste difdalla libreria SWI-Prolog, ma facile da rendere autonomo.)
Primo, singolo passaggio di semplificazione:
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).
Quindi, applicazione ripetuta di questi passaggi ai sottotermini e iterazione alla radice fino a quando non cambia più nulla:
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 ).
Per esempio:
?- formula_simple(~ ~ ~ ~ ~ a, Simple).
Simple = ~a.
Per la sostituzione di variabili con altri valori, prima un predicato per trovare variabili nelle formule:
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).
Durante il backtracking, verranno enumerate tutte le occorrenze di variabili in una formula, ad esempio:
?- formula_variable((p => q) <=> (~q => ~p), Var).
Var = p ;
Var = q ;
Var = q ;
Var = p ;
false.
Questa è l'unica fonte di non determinismo nella procedura di dimostrazione di seguito e puoi inserire un taglio dopo la formula_variablechiamata per impegnarti in una singola scelta.
Ora l'effettiva sostituzione di a Variablein a Formulacon 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].
E infine il prover, costruendo un termine di prova come la versione 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).
Una prova dell'esempio dalla domanda:
?- 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))) .
Tutte le sue prove:
?- 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.
Questo contiene molta ridondanza. Ancora una volta, questo perché formula_variableenumera le occorrenze delle variabili. Può essere reso più deterministico in vari modi a seconda delle proprie esigenze.
EDIT: L'implementazione di cui sopra formula_simpleè ingenua e inefficiente: ogni volta che fa una semplificazione di successo alla radice della formula, rivisita anche tutte le sottoformule. Ma su questo problema, non saranno possibili nuove semplificazioni delle sottoformule quando la radice sarà semplificata. Ecco una nuova versione che è più attenta a riscrivere prima completamente le sottoformule e quindi a ripetere solo le riscritture alla radice:
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 ).
Questo è notevolmente più veloce:
?- 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& ... & ...).
Modifica: come sottolineato nei commenti, il prover come scritto sopra può essere molto lento con formule leggermente più grandi. Il problema è che dimenticavo che alcuni operatori sono commutativi! Grazie jnmonette per averlo segnalato. Le regole di riscrittura devono essere espanse un po ':
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).
...
E con questo il prover si comporta bene.
Ecco uno scheletro di soluzione. Spero che possa aiutarti a riempire i buchi.
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)
).
Ora è necessario implementare reduce / 2 che applica le regole di riduzione (ricorsivamente nelle sottoformule) e branch / 2 che sostituisce in modo non deterministico un atomo della formula con top o bot, quindi chiama ricorsivamente derive / 2. Qualcosa di simile a:
branch(Formula, D):-
pickAtom(Formula, Atom),
(
Rep=top
;
Rep=bot
),
replace(Formula, Atom, Rep, Formula1),
derive(Formula1,D).
Sembra che questo metodo di forza bruta sia più vecchio (*) e poiché il codice Prolog è così piccolo, si adatta persino alla tasca dei pantaloni:
Ecco un'implementazione completa. Il taglio viene utilizzato solo per dare la priorità alla riscrittura e corrisponde praticamente alle regole Haskell. Tranne che Haskell potrebbe non avere una variabile logica del tipo di dati come 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).
Il codice non è puro Prolog e utilizza non logici var / 1, (==) / 2, ecc. Meta programmazione. Come Boole riduciamo linearmente ed eseguiamo una congiunzione delle due sostituzioni, quindi eseguiamo la divisione Quine senza alcuna ramificazione e tramite un unico fronte:
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).
In precedenza usiamo copy_term / 2 per eseguire la sostituzione. L'idea è stata presa in prestito dalla libreria lambda di Ulrich Neumerkels. Dobbiamo anche rendere disponibile = <e =: = in eval / 2 e simp / 2. Per il codice sorgente completo vedere qui . Ecco alcuni esempi di esecuzione in uno dei tuoi ISO Prolog preferiti:
?- 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].
(*) Da:
U. Martin e T. Nipkow. Unificazione booleana: la storia finora.
In Unification, pagine 437–455. Academic Press, Londra, 1990.