Subsunción theta

La subsunción theta (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 un concepto fundamental en la programación lógica inductiva . Decidir si una cláusula dada subsume a otra mediante la subsunción theta 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${\textstyle c_{1}}$θ-subsume una cláusula${\textstyle c_{2}}$Si hay una sustitución${\displaystyle \theta }$de tal manera que la cláusula obtenida mediante la aplicación${\textstyle \theta }$a${\textstyle c_{1}}$es un subconjunto de${\textstyle c_{2}}$. ^{[ 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${\textstyle c_{1}}$θ-subsume una cláusula ${\textstyle c_{2}}$, entonces${\textstyle c_{1}}$lógicamente implica${\textstyle c_{2}}$Sin embargo, lo contrario no es cierto: una cláusula puede implicar lógicamente otra cláusula, pero no subsumirla mediante θ.

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 el contexto 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 mediante θ, existe una única cláusula más corta salvo renombramiento de variables, que puede calcularse eficazmente. La clase de cocientes con respecto a esta relación de equivalencia es un retículo completo , que tiene cadenas ascendentes e descendentes infinitas. 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 generalizaciones menos generales de conjuntos de cláusulas. ^{[ 5 ]} En 1977, Lewis D. Baxter demuestra que la θ-subsunción es NP-completa, ^{[ 6 ]} y la obra fundamental de 1979 sobre problemas NP-completos, Computers and Intractability , la 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 eliminar cláusulas redundantes. ^{[ 7 ]} Además, la θ-subsunción es la noción de implicación más destacada 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 ]} También se utiliza para comprobar si una cláusula abarca un ejemplo y para determinar si un par de cláusulas dado es redundante. ^{[ 2 ]}

• Baxter, Lewis Denver (septiembre de 1977). La complejidad de la unificación (PDF) (Tesis). Universidad de Waterloo.
• De Raedt, Luc (2008). Aprendizaje lógico y relacional . Tecnologías cognitivas. Berlín, Heidelberg: Springer. Bibcode : 2008lrl..book.....D . doi : 10.1007/978-3-540-68856-3 . ISBN 978-3-540-20040-6.
• Kietz, Jörg-Uwe; Lübbe, Marcus (1994). «Un algoritmo de subsunción eficiente para la programación lógica inductiva» . Actas de Machine Learning 1994. Elsevier. págs. 130–138 . doi : 10.1016/b978-1-55860-335-6.50024-6 . ISBN  9781558603356. Consultado el 26 de noviembre de 2023 .
• Plotkin, Gordon D. (1970). Métodos automáticos de inferencia inductiva (PDF) (PhD). Universidad de Edimburgo. hdl : 1842/6656 .
• Robinson, JA (1965). "Una lógica orientada a máquinas basada en el principio de resolución" . Journal of the ACM . 12 (1): 23– 41. doi : 10.1145/321250.321253 . S2CID 14389185 . 
• Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin (noviembre de 2022). "Un marco integral para la demostración del teorema de saturación" . Journal of Automated Reasoning . 66 (4): 499– 539. doi : 10.1007/s10817-022-09621-7 . ISSN 0168-7433 . PMC 9637109. PMID 36353684 .