Unificación de resolución lógica de primer orden

Question

Suponiendo que he mostrado parte de la base de conocimiento en el formato clausal:

[1] p1(banana).

[2] not p1(X) or p2(Y).
[3] p1(X) or not p3(F).

... y más reglas.

La mayoría de los libros harían algo como esto:

[1,2] {X=banana} p2(Y).

y más pasos.

Primera pregunta: ¿Es igualmente correcto hacer algo como Follows:

[2,3] {X=X} p2(Y) or not p3(F).

y luego continúe con la resolución.

Segunda pregunta: ¿Qué pasaría si se usaron diferentes variables en cada cláusula? ¿Podría hacer lo mismo que el anterior? Por ejemplo, teníamos:

[2] not p1(X1) or p2(Y1).
[3] p1(X2) or not p3(F2).

[2,3] {X1=X2} p2(Y) or not p3(F2).

Gracias de antemano

Answer 1

Suponiendo que $ x $ aquí hay una variable, en lugar de una proposición atómica, luego primero debe especificar cuál es la cuantificación para 2 y 3. Supongo que debería ser

$ forall x, y neg p1 (x) vee p2 (y) $, y de manera similar para 3. En este caso, lo que se puede hacer es reemplazar $ x $ y $ y $ con cada propuesta atómica disponible, en para obtener una base de conocimiento proposicional y trabajar en eso.

Lo que sugiere hacer con 2,3 es sólido solo bajo cuantificación universal, pero si solo tiene cuantificación universal, es de hecho.

Para su segunda pregunta: el nombre de la variable no significa nada, por lo que su sustitución también es sólida. De hecho, el reclamo $ forall y, p (y) $ es equivalente a $ forall z, p (z) $. Primero puedes cambiar los nombres, si te hace feliz :)

Observaré que, por lo general, en las pruebas guiadas por resolución, es más útil resolver una expresión concreta con una regla cuantificada. Por ejemplo, resolviendo $ P (a) $ con $ FORALL XP (X) a Q (x) $ para obtener $ Q (a) $. Esto es más probable (heurísticamente) de llevarlo hacia la prueba de un reclamo.