Desprendimiento condensado

El método de separación condensada (Regla D) permite hallar la conclusión más general posible dadas dos proposiciones lógicas formales. Fue desarrollado por el lógico irlandés Carew Meredith en la década de 1950 e inspirado por la obra de Łukasiewicz . ^{[ 1 ]}

Una regla de desprendimiento (a menudo denominada modus ponens ) dice: "Dado que${\displaystyle p}$implica${\displaystyle q}$y dado${\displaystyle p}$inferir${\displaystyle q}$"

El desprendimiento condensado va un paso más allá y dice: "Dado que${\displaystyle p}$implica${\displaystyle q}$y dado un${\displaystyle r}$, utilice un unificador de${\displaystyle p}$y${\displaystyle r}$hacer${\displaystyle p}$y${\displaystyle r}$Si es lo mismo, entonces utilice una regla estándar de separación."

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

Diversos unificadores pueden producir expresiones con un número variable de variables libres . Algunas expresiones unificadoras posibles 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 el desprendimiento condensado, 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 un unificador inferior al 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, incluyendo todas sus instancias de sustitución (salvo el cambio de nombre de las variables), puede generarse únicamente mediante el desprendimiento condensado. Por ejemplo, si${\displaystyle p\rightarrow p}$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.${\displaystyle (p\rightarrow p)\rightarrow (p\rightarrow p)}$mediante el uso de una demostración 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 del 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 bien es una instancia de sustitución de algo que puede generarse únicamente 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.

Dado que una premisa mayor y una premisa menor determinadas determinan de forma unívoca la conclusión (salvo que se cambie el nombre de alguna variable), Meredith observó que solo era necesario indicar qué dos enunciados estaban involucrados y que la separación condensada podía utilizarse sin necesidad de ninguna otra notación. Esto dio lugar a la «notación D» para las demostraciones . Esta notación utiliza el operador «D» para indicar la separación condensada y toma dos argumentos en una cadena de notación prefija estándar . Por ejemplo, si se tienen cuatro axiomas, una demostración típica en notación D podría ser: DD12D34, que muestra un paso de separación condensada utilizando el resultado de dos pasos de separación condensada previos, el primero de los cuales utilizó los axiomas 1 y 2, y el segundo los axiomas 3 y 4.

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

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

Para la demostración automatizada de teoremas, el método de separación condensada presenta varias ventajas sobre el modus ponens puro y la sustitución uniforme.

En una demostración que utiliza el modus ponens y la sustitución, se dispone de un número infinito de opciones para sustituir las variables. Esto implica un número infinito de posibles pasos siguientes. Con el método de separación condensada, solo existen un número finito de posibles pasos siguientes en una demostración, concretamente las variantes más generales de los pasos o axiomas anteriores combinados.

La notación D para demostraciones de separación condensadas completas permite una descripción sencilla de las demostraciones para su catalogación y búsqueda. Una demostración completa típica de 15 pasos ocupa solo 15 caracteres en notación D (sin incluir el enunciado de los axiomas). Puede aumentar ligeramente si se hacen referencia a más de nueve axiomas o teoremas; por ejemplo, se podría escribir DD2.10D11DD5.6D9D35.3 usando puntos para separar números de varias cifras (pero también DD2aDbDD56D9Dz3 para la misma demostración con hasta 35 números de referencia).

• 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 separación condensada» (PDF) . En D. Kapur (ed.). Actas de la 11.ª Conferencia Internacional sobre Deducción Automatizada (CADE) . LNCS. Vol.  607. Springer. págs. 209–223 .