El desapego condensado (Regla D) es un método para encontrar la conclusión más general posible dadas dos declaraciones lógicas 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]
Una regla de separación (a menudo denominada modus ponens ) dice:
"Dado eso implica , y dado , inferir ".
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".
Una sustitución A que cuando se aplica produce , y una sustitución B que cuando se aplica produce , se denominan unificadores de y .
Varios unificadores pueden producir expresiones con distintos números 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 sólo un cambio de nombre de variable), entonces esa otra se denomina "más general".
Si se utiliza el unificador más general en el desapego condensado, entonces el resultado lógico es la conclusión más general que se puede hacer en la inferencia dada con la segunda expresión dada. Dado que cualquier inferencia más débil que pueda obtenerse es una instancia de sustitución de la más general, en la práctica nunca se utiliza nada menos que el unificador más general.
Algunas lógicas, como el cálculo proposicional clásico , tienen un conjunto de axiomas definitorios con la propiedad "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), puede generarse únicamente mediante separación condensada. Por ejemplo, si es un teorema de un sistema D-completo, el desprendimiento condensado puede probar no solo ese teorema sino también su instancia de sustitución mediante el uso de una demostración más larga. Tenga en cuenta que la "completitud D" es una propiedad de una base axiomática de un sistema, no una propiedad intrínseca de un sistema lógico en sí. [2]
JA Kalman demostró que cualquier conclusión que pueda generarse mediante una secuencia de sustitución uniforme (todas las instancias de una variable se reemplazan con el mismo contenido) y pasos de modus ponens puede generarse únicamente mediante desprendimiento condensado o es una instancia de sustitución de algo que puede ser generado únicamente por desapego condensado. [1] Esto hace que el desapego condensado sea útil para cualquier sistema lógico que tenga modus ponens y sustitución, independientemente de si es D-completo o no.
Dado que una premisa mayor determinada y una premisa menor determinada determinan de forma única la conclusión (hasta el cambio de nombre variable), Meredith observó que sólo era necesario señalar qué dos declaraciones 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 pruebas . 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 condensado utilizando el resultado de dos pasos de separación condensados anteriores, el primero de los cuales usó los axiomas 1 y 2, y el segundo de que utilizó los axiomas 3 y 4.
Esta notación, además de utilizarse en algunos demostradores de teoremas automatizados, aparece en ocasiones en catálogos de demostraciones. Por ejemplo, la base de datos de "demostraciones más cortas conocidas" del proyecto mmsolitaire de Metamath presenta 196 teoremas con dichas demostraciones. [3]
El uso de la unificación por desapego condensado es anterior a la técnica de resolución de demostración automatizada de teoremas que se introdujo en 1965. [4] [5]
Para la demostración automatizada de teoremas, el desprendimiento condensado tiene una serie de ventajas sobre el modus ponens bruto y la sustitución uniforme.
En un Modus Ponens y una prueba de sustitución, tienes un número infinito de opciones sobre lo que puedes sustituir por variables. Esto significa que tienes un número infinito de posibles próximos pasos. Con el desapego condensado sólo hay un número finito de posibles siguientes pasos en una demostración. [ se necesita aclaración ]
La notación D para pruebas de separación condensadas completas permite una fácil descripción de las pruebas para catalogación y búsqueda. Una prueba típica completa de 30 pasos tiene menos de 60 caracteres en notación D (excluyendo la declaración de los axiomas).
