En lógica matemática y programación lógica , una cláusula de Horn es una fórmula lógica de una forma particular similar a una regla que le otorga propiedades útiles para su uso en programación lógica, especificación formal y teoría de modelos . Las cláusulas de Horn llevan el nombre del lógico Alfred Horn , quien señaló por primera vez su importancia en 1951. [1]
Una cláusula de Horn es una cláusula (una disyunción de literales ) con como máximo un literal positivo, es decir , innecesario .
A la inversa, una disyunción de literales con como máximo un literal negado se denomina cláusula de cuerno dual .
Una cláusula de Horn con exactamente un literal positivo es una cláusula definida o una cláusula de Horn estricta ; [2] una cláusula definida sin literales negativos es una cláusula unitaria , [3] y una cláusula unitaria sin variables es un hecho ; [4] . Una cláusula de Horn sin un literal positivo es una cláusula de meta . Tenga en cuenta que la cláusula vacía, que no consta de literales (lo que equivale a falso ) es una cláusula de objetivo. Estos tres tipos de cláusulas de Horn se ilustran en el siguiente ejemplo proposicional :
Todas las variables de una cláusula se cuantifican implícitamente de forma universal y el alcance es la cláusula completa. Así, por ejemplo:
Las cláusulas de Horn juegan un papel básico en la lógica constructiva y la lógica computacional . Son importantes en el teorema automatizado que demuestra por resolución de primer orden , ya que el resolutivo de dos cláusulas de Horn es en sí mismo una cláusula de Hornos y el resolutivo de una cláusula de gol y una cláusula definitiva es una cláusula de meta. Estas propiedades de las cláusulas de Horn pueden conducir a una mayor eficiencia de demostrar un teorema: la cláusula de meta es la negación de este teorema; ver cláusula de metaen la tabla de arriba. Intuitivamente, si deseamos probar φ, asumimos ¬φ (el objetivo) y verificamos si tal suposición conduce a una contradicción. Si es así, entonces φ debe aguantar. De esta manera, una herramienta de prueba mecánica necesita mantener solo un conjunto de fórmulas (supuestos), en lugar de dos conjuntos (supuestos y (sub) metas).