En lógica matemática y programación lógica , una cláusula de Horn es una fórmula lógica de una forma similar a una regla particular 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 significado 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 , no negado .
Por el contrario, una disyunción de literales con a lo sumo un literal negado se denomina cláusula dual-Horn .
Una cláusula Horn con exactamente un literal positivo es una cláusula definida [2] o una cláusula Horn estricta ; [3] una cláusula definida sin literales negativos es una cláusula unitaria , [4] y una cláusula unitaria sin variables es un hecho ; [5] . Una cláusula de Horn sin un literal positivo es una cláusula de objetivo . Tenga en cuenta que la cláusula vacía, que no consta de literales (lo que equivale a false ), es una cláusula de objetivo. Estos tres tipos de cláusulas de Horn se ilustran en el siguiente ejemplo proposicional :
Todas las variables en una cláusula se cuantifican implícitamente universalmente y el alcance es la cláusula completa. Así, por ejemplo:
Las cláusulas Horn juegan un papel básico en la lógica constructiva y la lógica computacional . Son importantes en la demostración automatizada de teoremas por resolución de primer orden , porque el resolutivo de dos cláusulas de Horn es en sí mismo una cláusula de Horn, y el resolutivo de una cláusula de objetivo y una cláusula definida es una cláusula de objetivo. Estas propiedades de las cláusulas de Horn pueden conducir a una mayor eficiencia en la demostración de un teorema: la cláusula de objetivo es la negación de este teorema; ver cláusula de objetivoen la tabla anterior. Intuitivamente, si queremos probar φ, asumimos ¬φ (el objetivo) y verificamos si tal suposición conduce a una contradicción. Si es así, entonces φ debe cumplirse. De esta forma, una herramienta de prueba mecánica necesita mantener solo un conjunto de fórmulas (suposiciones), en lugar de dos conjuntos (suposiciones y (sub)objetivos).