Implementación del prólogo del algoritmo de Quine para la lógica proposicional clásica (en los "Métodos de lógica" de Quine)
Solo conozco un probador que traduce el algoritmo que Quine dio para la lógica proposicional clásica en su libro Methods of Logic (Harvard University Press, 1982, cap. 1 sec.5, págs. 33-40), este probador está en Haskell y está aquí: el algoritmo de Quine en Haskell
Intenté traducir el algoritmo de Quine en Prolog, pero hasta ahora no lo he conseguido. Es una lástima porque es un algoritmo eficiente y una traducción de Prolog sería interesante. Voy a describir este algoritmo. El único código de Prolog que doy al principio es la lista de operadores que serían útiles para probar el 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
Las constantes de verdad son topy botpara, respectivamente, verdadero y falso . El algoritmo comienza de la siguiente manera: Para cualquier fórmula proposicional F , haga dos copias de la misma y reemplace el átomo que tiene la mayor ocurrencia en F por topen la primera copia y por boten la segunda copia, y luego aplique las siguientes diez reglas de reducción una regla a la vez durante tantas veces como sea posible, para cada una de las copias:
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
Por supuesto, también tenemos las siguientes reglas para la negación y la doble negación:
1. ~bot --> top
2. ~top --> bot
3. ~~p --> p
Cuando no hay ni toptampoco boten la fórmula por lo que ninguna de las reglas se aplican, se dividió de nuevo y recoger un átomo de sustituirlo por top y por la botde otra mesa de dos caras. La fórmula F se prueba si y solo si el algoritmo termina con topen todas las copias, y no se puede probar, de lo contrario.
Ejemplo:
(p => q) <=> (~q => ~p)
(p => top) <=> (bot => ~p) (p => bot) <=> (top => ~p)
top <=> top ~p <=> ~p
top top <=> top bot <=> bot
top top
Está claro que el algoritmo de Quine es una optimización del método de tablas de verdad, pero a partir de códigos de programa del generador de tablas de verdad, no logré conseguirlo en código Prolog.
Una ayuda al menos para empezar sería bienvenida. De antemano muchas gracias.
EDITAR por Guy Coder
Esto se publica dos veces en el foro SWI-Prolog que tiene una discusión animada y donde los probadores Prolog se publican pero no se reproducen en esta página.
Respuestas
El código Haskell me pareció complicado. Aquí hay una implementación basada en la descripción del algoritmo dada en la pregunta. (Usando maplisty difdesde la biblioteca SWI-Prolog, pero fácil de hacer autónomo).
Primero, pasos simples de simplificación:
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).
Luego, repita la aplicación de estos pasos a subterráneos e iteración en la raíz hasta que nada cambie más:
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 ).
Por ejemplo:
?- formula_simple(~ ~ ~ ~ ~ a, Simple).
Simple = ~a.
Para el reemplazo de variables por otros valores, primero un predicado para encontrar variables en fórmulas:
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).
Al retroceder, esto enumerará todas las apariciones de variables en una fórmula, por ejemplo:
?- formula_variable((p => q) <=> (~q => ~p), Var).
Var = p ;
Var = q ;
Var = q ;
Var = p ;
false.
Esta es la única fuente de no determinismo en el procedimiento de prueba a continuación, y puede insertar un corte después de la formula_variablellamada para comprometerse con una sola opción.
Ahora, el reemplazo real de a Variableen a Formulapor 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].
Y finalmente el prover, construyendo un término de prueba como la versión de 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 prueba del ejemplo de la pregunta:
?- 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))) .
Todas sus pruebas:
?- 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.
Esto contiene mucha redundancia. Nuevamente, esto se debe a que formula_variableenumera las apariciones de variables. Se puede hacer más determinista de varias formas dependiendo de los requisitos de cada uno.
EDITAR: La implementación anterior de formula_simplees ingenua e ineficiente: cada vez que hace una simplificación exitosa en la raíz de la fórmula, también revisa todas las subfórmulas. Pero en este problema, no serán posibles nuevas simplificaciones de las subfórmulas cuando se simplifique la raíz. Aquí hay una nueva versión que es más cuidadosa para reescribir primero completamente las subfórmulas y luego solo iterar las reescrituras en la raíz:
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 ).
Esto es considerablemente más rápido:
?- 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& ... & ...).
Editar: como se señaló en los comentarios, el probador como se escribió anteriormente puede ser muy lento en fórmulas un poco más grandes. ¡El problema es que olvidé que algunos operadores son conmutativos! Gracias jnmonette por señalar esto. Las reglas de reescritura deben expandirse un poco:
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).
...
Y con esto el prover se comporta muy bien.
Aquí hay un esqueleto de solución. Espero que pueda ayudarte a llenar los agujeros.
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)
).
Ahora necesita implementar reduce / 2 que aplica las reglas de reducción (recursivamente en las subfórmulas), y branch / 2 que reemplaza de forma no determinista un átomo de la fórmula con top o bot, luego llama de forma recursiva a derivar / 2. Algo como:
branch(Formula, D):-
pickAtom(Formula, Atom),
(
Rep=top
;
Rep=bot
),
replace(Formula, Atom, Rep, Formula1),
derive(Formula1,D).
Parece que este método de fuerza bruta es más antiguo (*), y como el código de Prolog es tan pequeño que incluso cabe en el bolsillo de tus pantalones:
Aquí hay una implementación completa. El corte solo se usa para priorizar la reescritura y corresponde prácticamente a las reglas de Haskell. Excepto que Haskell podría no tener una variable lógica de tipo de datos como 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).
El código no es puro Prolog y usa meta programación var / 1, (==) / 2, etc. no lógicas. Al igual que Boole, reducimos linealmente y realizamos una conjunción de las dos sustituciones, por lo que hacemos la división de Quine sin algunas ramificaciones y mediante un solo frente:
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).
En lo anterior usamos copy_term / 2 para hacer la sustitución. La idea está tomada de la biblioteca lambda de Ulrich Neumerkels. Necesitamos también hacer disponible = <y =: = en eval / 2 y simp / 2. Para obtener el código fuente completo, consulte aquí . A continuación, se muestran ejecuciones de ejemplo en cualquiera de sus prólogos ISO favoritos:
?- 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].
(*) De:
U. Martin y T. Nipkow. Unificación booleana: la historia hasta ahora.
En Unificación, páginas 437–455. Academic Press, Londres, 1990.