La theta-subsunción (θ-subsunción, o simplemente subsunción) es una relación decidible entre dos cláusulas de primer orden que garantiza que una cláusula implica lógicamente a la otra. Fue introducida por primera vez por John Alan Robinson en 1965 y se ha convertido en una noción fundamental en la programación lógica inductiva . Decidir si una cláusula dada θ-subsume a otra es un problema NP-completo .
Una cláusula, es decir, una disyunción de literales de primer orden , puede considerarse como un conjunto que contiene todos sus disyuntos.
Con esta convención, una cláusula θ-subsume una cláusula si hay una sustitución tal que la cláusula obtenida al aplicar a es un subconjunto de . [1]
La θ-subsunción es una relación más débil que la implicación lógica , es decir, siempre que una cláusula θ-subsume una cláusula , entonces implica lógicamente . Sin embargo, lo inverso no es cierto: una cláusula puede implicar lógicamente otra cláusula, pero no θ-subsumirla.
La θ-subsunción es decidible; más precisamente, el problema de si una cláusula θ-subsume a otra es NP-completo en la longitud de las cláusulas. Esto sigue siendo cierto cuando se restringe la configuración a pares de cláusulas de Horn . [2]
Como relación binaria entre cláusulas de Horn, la θ-subsunción es reflexiva y transitiva . Por lo tanto, define un preorden . No es antisimétrica , ya que diferentes cláusulas pueden ser variantes sintácticas entre sí. Sin embargo, en cada clase de equivalencia de cláusulas que se θ-subsumen mutuamente, hay una cláusula más corta única hasta el cambio de nombre de la variable, que se puede calcular de manera efectiva. La clase de cocientes con respecto a esta relación de equivalencia es un retículo completo , que tiene cadenas infinitas ascendentes y descendentes. Un subconjunto de este retículo se conoce comográfico de refinamiento .[3]
La θ-subsunción fue introducida por primera vez por J. Alan Robinson en 1965 en el contexto de la resolución , [4] y fue aplicada por primera vez a la programación lógica inductiva por Gordon Plotkin en 1970 para encontrar y reducir las generalizaciones menos generales de conjuntos de cláusulas. [5] En 1977, Lewis D. Baxter demuestra que la θ-subsunción es NP-completa, [6] y el trabajo seminal de 1979 sobre problemas NP-completos, Computers and Intractability , lo incluye entre su lista de problemas NP-completos. [2]
Los demostradores de teoremas basados en el cálculo de resolución o superposición utilizan la θ-subsunción para podar cláusulas redundantes. [7] Además, la θ-subsunción es la noción más destacada de implicación utilizada en la programación lógica inductiva , donde es la herramienta fundamental para determinar si una cláusula es una especialización o una generalización de otra. [1] Se utiliza además para comprobar si una cláusula cubre un ejemplo y para determinar si un par dado de cláusulas es redundante. [2]
