Desprendimiento condensado

El desapego condensado (Regla D) es un método para hallar la conclusión más general posible a partir de dos enunciados lógicos formales. Fue desarrollado por el lógico irlandés Carew Meredith en la década de 1950 e inspirado en el trabajo de Łukasiewicz . ^[1]

Descripción informal

Una regla de desapego (a menudo denominada modus ponens ) dice:
"Dado que implica , y dado , se infiere ". ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle p}$ ${\displaystyle q}$

El desapego condensado va un paso más allá y dice:
"Dado que implica , y dado un , use un unificador de y para hacer y lo mismo, entonces use una regla estándar de desapego". ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle r}$ ${\displaystyle p}$ ${\displaystyle r}$ ${\displaystyle p}$ ${\displaystyle r}$

Una sustitución A que cuando se aplica a produce , y una sustitución B que cuando se aplica a produce , se denominan unificadores de y . ${\displaystyle p}$ ${\displaystyle t}$ ${\displaystyle r}$ ${\displaystyle t}$ ${\displaystyle p}$ ${\displaystyle r}$

Varios unificadores pueden producir expresiones con diferentes cantidades de variables libres . Algunas posibles expresiones unificadoras son instancias de sustitución de otras. Si una expresión es una instancia de sustitución de otra (y no solo un cambio de nombre de variable), entonces esa otra se denomina "más general".

Si se utiliza el unificador más general en la separación condensada, entonces el resultado lógico es la conclusión más general que se puede obtener en la inferencia dada con la segunda expresión dada. Dado que cualquier inferencia más débil que se pueda obtener es una instancia de sustitución de la más general, en la práctica nunca se utiliza nada que no sea el unificador más general.

Algunas lógicas, como el cálculo proposicional clásico , tienen un conjunto de axiomas definitorios con la propiedad de "D-completitud". Si un conjunto de axiomas es D-completo, entonces cualquier teorema válido del sistema, incluidas todas sus instancias de sustitución (hasta el cambio de nombre de la variable), se puede generar solo mediante desprendimiento condensado. Por ejemplo, si es un teorema de un sistema D-completo, el desprendimiento condensado puede demostrar no solo ese teorema sino también su instancia de sustitución utilizando una prueba más larga. Nótese que la "D-completitud" es una propiedad de una base axiomática para un sistema, no una propiedad intrínseca de un sistema lógico en sí. ^[2] ${\displaystyle p\rightarrow p}$ ${\displaystyle (p\rightarrow p)\rightarrow (p\rightarrow p)}$

JA Kalman demostró que cualquier conclusión que pueda generarse mediante una secuencia de pasos de sustitución uniforme (todas las instancias de una variable se reemplazan con el mismo contenido) y modus ponens puede generarse solo mediante desprendimiento condensado, o es una instancia de sustitución de algo que puede generarse solo mediante desprendimiento condensado. ^[1] Esto hace que el desprendimiento condensado sea útil para cualquier sistema lógico que tenga modus ponens y sustitución, independientemente de si es D-completo o no.

Notación D

Dado que una premisa mayor dada y una premisa menor dada determinan de manera única la conclusión (hasta el cambio de nombre de la variable), Meredith observó que solo era necesario señalar cuáles dos afirmaciones estaban involucradas y que la separación condensada se puede utilizar sin necesidad de ninguna otra notación. Esto llevó a la "notación D" para las demostraciones . Esta notación utiliza el operador "D" para indicar separación condensada y toma 2 argumentos, en una cadena de notación de prefijo estándar . Por ejemplo, si tiene cuatro axiomas, una demostración típica en notación D podría verse así: DD12D34 que muestra un paso de separación condensada utilizando el resultado de dos pasos de separación condensada anteriores, el primero de los cuales utilizó los axiomas 1 y 2, y el segundo de los cuales utilizó los axiomas 3 y 4.

Esta notación, además de utilizarse en algunos demostradores automáticos de teoremas, aparece a veces en catálogos de demostraciones. Por ejemplo, la base de datos de "demostraciones más breves conocidas" del proyecto mmsolitaire de Metamath contiene 196 teoremas con dichas demostraciones. ^[3]

El uso de la unificación en el desprendimiento condensado es anterior a la técnica de resolución de demostración automática de teoremas que se introdujo en 1965. ^{[4] [5]}

Ventajas

Para la demostración automática de teoremas, el desprendimiento condensado tiene una serie de ventajas sobre el modus ponens puro y la sustitución uniforme.

En una demostración de Modus Ponens y sustitución, tienes una cantidad infinita de opciones para lo que puedes sustituir por variables. Esto significa que tienes una cantidad infinita de posibles pasos siguientes. Con el desapego condensado, solo hay una cantidad finita de posibles pasos siguientes en una demostración. ^{[ Aclaración necesaria ]}

La notación D para demostraciones condensadas de desprendimiento completas permite una descripción sencilla de las demostraciones para su catalogación y búsqueda. Una demostración completa típica de 30 pasos tiene menos de 60 caracteres en notación D (excluyendo el enunciado de los axiomas).

Referencias

1. JA Kalman (diciembre de 1983). "El desapego condensado como regla de inferencia". Studia Logica . 42 (4): 443–451. doi :10.1007/BF01371632. S2CID  121221548.
2. N. Megill y M. Bunder (marzo de 1996). "Lógicas D-completas más débiles" (PDF) . J. Igpl . 4 (2): 215–225. CiteSeerX 10.1.1.100.6257 . doi :10.1093/jigpal/4.2.215. 
3. "Las pruebas más breves conocidas de los teoremas del cálculo proposicional de Principia Mathematica". Metamath . Consultado el 9 de septiembre de 2023 .
4. CA Meredith y AN Prior (1963). "Notas sobre la axiomática del cálculo proposicional". Notre Dame J. Formal Logic . 4 (3): 171–187. doi : 10.1305/ndjfl/1093957574 .
5. JA Robinson (1965). "Una lógica orientada a máquinas basada en el principio de resolución". Revista de la ACM . 12 (1): 23–41. doi : 10.1145/321250.321253 . S2CID  14389185.

• Hindley, J. Roger (1993), "Lógicas BCK y BCI, desprendimiento condensado y la propiedad 2", Notre Dame Journal of Formal Logic , 34 (2): 231–250, doi : 10.1305/ndjfl/1093634655 , MR  1231287
• William McCune y Larry Wos (1992). "Experimentos en deducción automatizada con desprendimiento condensado" (PDF) . En D. Kapur (ed.). Proc. 11th International Conference on Automated Deduction (CADE) . LNCS. Vol. 607. Springer. págs. 209–223.