Para ayudarme a entender la paramodulación en general estoy tratando de entender la particular Prover9 ejemplo más abajo. Prover9 es un probador de teoremas automatizado para lógica de primer orden y ecuacional que utiliza la paramodulación y la resolución.
En el Salida de Prover9 abajo hay tres axiomas en las líneas 1, 2 y 3. El teorema a demostrar, o meta, aparece en la línea 4. Los axiomas se transforman en forma de cláusula en las líneas 5, 6 y 7. El objetivo se niega en la línea 8. El objetivo negado se utilizará para la resolución en la línea 19. La justificación de la derivación de cada línea aparece entre corchetes al final de la misma. De acuerdo con la Glosario Prover9 :
Una inferencia de paramodulación consiste en dos padres y un hijo. El padre padre que contiene la igualdad utilizada para la sustitución es el padre from o la cláusula from, la igualdad es el literal from, y el lado lado de la igualdad que se unifica con el término que se sustituye es el término from. El término reemplazado es el término into, el literal que contiene el término sustituido es el literal into, y el padre que contiene el término reemplazado es el padre into o la cláusula into.
No entiendo la derivación de la línea 9. Intuitivamente, puedo ver que la línea 9 es la niño de padre líneas 5 y 6. A partir de los axiomas se pueden igualar los lados izquierdos de ambas líneas. Llamaré a esta igualdad 9a.
9a turn(move(turn(move(turn(move(turn(move(x)))))))) = turn(turn(turn(turn(x))))Ahora la línea 9 tiene los primeros términos, turn(...) a la izquierda y a la derecha de la igualdad en 9a eliminado. La izquierda y la derecha de la línea 9 son subtermas de la izquierda y la derecha de la línea 9a.
9 move(turn(move(turn(move(turn(move(x))))))) = turn(turn(turn(x))). para(6(a,1),5(a,1,1,1,1)),flip(a)].Desde mi punto de vista, quizás incorrecto, del razonamiento ecuacional, a partir de dos términos $a$ y $b$ con $a=b$ podemos concluir $turn(a) = turn(b)$ . Desde mi ingenuo punto de vista este razonamiento permitiría pasar de las 9 a las 9a, pero no al revés.
Por el momento, no me preocupan demasiado las demás líneas de la prueba. Se agradecería cualquier explicación de cómo se dedujo la línea 9.
Salida de Prover9
1 (all p turn(turn(turn(turn(p)))) = p) # label(non_clause). [assumption].
2 (all p turn(move(turn(move(turn(move(turn(move(p)))))))) = p) # label(non_clause). [assumption].
3 (all p turn(turn(move(turn(turn(move(p)))))) = p) # label(non_clause). [assumption].
4 (all p turn(turn(turn(move(turn(move(p)))))) = move(turn(turn(turn(move(turn(p))))))) # label(non_clause) # label(goal). [goal].
5 turn(turn(turn(turn(x)))) = x. [clausify(1)].
6 turn(move(turn(move(turn(move(turn(move(x)))))))) = x. [clausify(2)].
7 turn(turn(move(turn(turn(move(x)))))) = x. [clausify(3)].
8 move(turn(turn(turn(move(turn(c1)))))) != turn(turn(turn(move(turn(move(c1)))))). [deny(4)].
9 move(turn(move(turn(move(turn(move(x))))))) = turn(turn(turn(x))). [para(6(a,1),5(a,1,1,1,1)),flip(a)].
11 move(turn(turn(move(x)))) = turn(turn(x)). [para(7(a,1),5(a,1,1,1)),flip(a)].
12 move(turn(move(turn(move(turn(turn(turn(x)))))))) = turn(move(x)). [para(11(a,1),9(a,1,1,1,1,1,1,1)),rewrite([5(13)])].
16 move(turn(move(turn(move(x))))) = turn(move(turn(x))). [para(5(a,1),12(a,1,1,1,1,1,1))].
18 move(turn(turn(turn(move(turn(x)))))) = turn(turn(turn(move(turn(move(x)))))). [para(16(a,1),11(a,1,1,1,1))].
19 $F. [resolve(18,a,8,a)].El ejemplo se refiere a un robot que se mueve a través de una red de VanHorebeek y Lewi también en libro . Aquí está relacionado puesto de paramodulación .
