¿Una explicación sencilla, pero no superficial, de lo que significa "paramodulación" en el contexto de la demostración automatizada de teoremas?

Question

Moderno demostradores automatizados de teoremas parecen ser paramodulación -basado.

Sólo tengo una comprensión superficial de lo que esto significa: derivamos una proposición cuya verdad está implícita en la verdad de [¿dos?] otras proposiciones.

Q : ¿Cuál es una explicación sencilla, pero no superficial, de lo que significa "paramodulación" en el contexto de la demostración automatizada de teoremas?

Buscar la definición en los periódicos siempre revela una montaña de jerga y notación que me asusta. (Aún no existe una página de Wikipedia sobre paramodulación: enlace .) Además, creo que una comprensión no superficial de los temas requiere ver a través de la notación y tener una "sensación" de lo que significa.

He aquí una prueba lógica de primer orden de que los grupos booleanos (grupos para los que $x^2=e$ para todos $x$ ) son abelianas (tomado de Robinson, Wos, Paramodulation and Theorem-proving in First-Order Theories with Equality [ pdf ]):

\begin{align*} 1. & & & f(ex)=x \\ 2. & & & f(xe)=x \\ 3. & & & f(xf(yz))=f(f(xy)z) \\ 4. & & & f(xx)=e \\ 5. & & & f(ab)=c \\ 6. & & & c \neq f(ab) \\ 7. & & & f(xe)=f(f(xy)y) & \text{4. into 3. with } \delta:f(yz) \\ 8. & & & x=f(f(xy)y) & \text{2. into 7. on } f(xe) \\ 9. & & & a=f(cb) & \text{5. into 8. on } f(xy) \\ 10. & & & f(yf(yz))=f(ez) & \text{4. into 3. on } f(xy) \\ 11. & & & f(yf(yz))=z & \text{1. into 10. on } f(ez) \\ 12. & & & f(ca)=b & \text{9. into 11. on } f(yz) \\ 13. & & & c=f(ba) & \text{12. into 8. on } f(xy) \\ 14. & & & \square & \text{resolved with 6.} \end{align*} Podemos ver que 1. a 3. son algunos de los axiomas de grupo, 4. es la propiedad booleana, y 5. se utiliza para formar una prueba por contradicción. Y los 7. a 14. se pueden deducir como se ha indicado (usando sustitución, renombrando variables y "multiplicando" ambos lados de la ecuación).

Answer 1

¿Conoce la técnica de refutación de teoremas de resolución ?

La regla de resolución es refutación-completa, en el sentido de que un conjunto de cláusulas es insatisfactible si y sólo si existe una derivación de la cláusula vacía utilizando únicamente la resolución.

Paramodulación es la modificación del sistema de resolución para gestionar igualdad .

Puede ver tratamientos detallados de resolución en Melvin Fitting, Lógica de primer orden y demostración automatizada de teoremas (1990) [para la paramodulación: página 231] o Chin-Liang Chang & Richard Char-Tung Lee, Lógica simbólica y demostración mecánica de teoremas (1973) [para la paramodulación: página 168].

De Chang & Char-Tung Lee, página 168:

Considere las siguientes cláusulas

$C_1 : P(a)$

$C_2 : a = b$ .

Desde $C_2$ es una igualdad $a = b$ sustituimos $b$ pour $a$ en $C_1$ para obtener una cláusula

$C_3 : P(b)$ .

En general, la regla de sustitución de igualdad puede enunciarse del siguiente modo: Si una cláusula $C_1$ contiene un término $t$ y si una cláusula de unidad $C_2$ es $t = s$ infiera una cláusula sustituyendo $s$ para una sola aparición de $t$ en $C_1$ .

La paramodulación es esencialmente una extensión de la regla de sustitución de igualdades anterior. Puede aplicarse a cualquier par de cláusulas (no necesariamente cláusulas unitarias). Por ejemplo, si una expresión $E$ (por ejemplo, una cláusula, un literal o un término) contiene un término $t$ denotaremos a veces $E$ por $E[t]$ . Además, si una sola ocurrencia de $t$ se sustituye por un término $s$ el resultado se denotará por $E[s]$ . Según esta convención, la paramodulación de las cláusulas suelo puede enunciarse como sigue: Si $C_1$ es $L[t] \lor C_1^*$ donde $L[t]$ es un literal que contiene un término $t$ y $C_1^*$ es una cláusula, y si $C_2$ es $t = s \lor C_2^*$ donde $C_2^*$ es una cláusula, entonces infiere la siguiente cláusula, llamada paramodulante :

$L[s] \cup C_1^* \cup C_2^*$ .