predicados - logica de primer orden prolog

Prólogo lógica de primer orden

Question

Estoy tratando de encontrar una forma de poner la siguiente expresión lógica de primer orden en Prolog:

(p(0) or p(1)) and not (p(0) and p(1))

Esto significa que debe responder de la siguiente manera a las consultas:

?- p(0)
Yes.
?- p(1)
Yes.
?- p(0),p(1).
No.

Traté de traducir la expresión lógica:

(p(0) or p(1)) and not (p(0) and p(1)) <=>
(not p(0) -> p(1)) and (p(0) -> not p(1)) <=>
p(0) <-> not p(1)

Utilizando la finalización de Clarks (que establece que cada teoría de definición se puede poner en un programa lógico dando las if-mitades), puedo obtener:

p(0) :- not p(1).

Desafortunadamente, esta teoría resultante es solo sonido (no derivará información falsa), pero no completa (por ejemplo: p (1) no se puede derivar). Esto es una consecuencia del teorema de Clarks.

¿Alguien sabe si hay una mejor solución? ¡Gracias!

Answer 1

En Prolog, si tanto p(0) como p(1) tienen éxito, entonces p(0),p(1) no puede fallar.

Eso significa que tendrías que construir tu propio pequeño intérprete, idear formas de representar tus objetivos y reglas para ello, y hacer en él tus preguntas, como

?- is_true( (p(0),p(1)) ).

Answer 2

Esto es sutil, pero en realidad estás equivocado. No debe esperar que p (0) esté relacionado. El establecimiento requeriría que p (0) sea verdadero en todos los modelos de la teoría. Pero esta teoría tiene dos modelos {p (1)} y {p (0)}.

Esto se estudia ampliamente en la literatura. Como señaló correctamente, la finalización de Clark no maneja estos casos. Lo que es peor, SLDNF cae en recursión infinita para

p(0) :- not p(1).
p(1) :- not p(0).

¿Cuál es la traducción más adecuada para las cláusulas definidas de su teoría?

Les ahorraré consejos sobre la definición de semántica diferente, pero si desean una solución rápida y práctica, sugiero cambiar a la Programación de conjunto de respuestas.

Aquí está el enlace a mi solucionador favorito (la guía también es agradable y autónoma): http://www.cs.uni-potsdam.de/clasp/

¡Disfrutar!

Answer 3

Lógicamente, ya en la lógica proposicional, no sigue (A v B) | - A y tampoco (A v B) | - B. La situación tampoco cambia si se agrega ~ (A y B).

La pregunta ahora es si la finalización de clark u otra cosa puede agregar más información predeterminada, de modo que finalmente tenemos T | - A y T | - B. Pero lógicamente tendremos T | - A & B.

Así que supongo que en un entorno normal es imposible de hacer, lo que le gustaría hacer.

Adiós

PD: Un ajuste no normal sería, por ejemplo, usar una relación de consecuencia crédula en lugar de una relación de consecuencia escéptica. La relación de consecuencia escéptica es:

T |- A iff forall M (if M |- T then M |- A)

La relación de consecuencia crédula es:

T |~ A iff exists M (M |- T and M |- A)

Es posible tener T | ~ A y T | ~ B, pero no T | ~ A & B, su (A v B) & ~ (A & B) sin ninguna información predeterminada ya es una teoría.

PSS: hay algunas formas de abusar de un sistema Prolog por razonamiento crédulo, aunque la base de Prologs es un razonamiento escéptico. El truco es usar la identidad T | ~ A = ~ (T | - ~ A).

Pero antes de que uno pueda aplicar esto a su ejemplo, uno tiene que resolver el problema de representar la disyunción en Prolog. Algunas disyunciones se pueden realizar a través de la siguiente identidad y el razonamiento hipotético :

(A v B -> C) == (A -> C) & (B -> C)

Answer 4

Si se permite introducir un término con nombre en su lógica de "destino", puede implementar una tummy 0 / ficticia:

t :- p(0), p(1), !, fail.
t :- p(0).
t :- p(1).

entonces si tenemos ambos

p(0).
p(1).

t / 0 fallará