La forma clausal y las cláusulas de Horn

Forma clausal

todas las variables de la formula estan cuantificadas universalmente, no es necesario incluir cuantificadores universales. Todos los cuantificadores se eliminan y todas las variables de la formula quedan cuantificadas implicitamente

la formula se compone de varias clausulas y cada clausula se compone de varias literales conectadas exclusivamente por conectores logicos OR. Entonces toda clausula es una disyuncion de literales

Las clausulas mismas se conectan exclusivamente mediante conectores logicos AND para construir una formula. Entonces la forma clausal de una formula es una conjuncion de clausulas

Clausula de Horn

Una cláusula de Horn es una regla de inferencia lógica con una serie de premisas (cero, una o más), y un único consecuente. Las cláusulas de Horn son las instrucciones  básicas del lenguaje de programación Prolog, de paradigma declarativo.

En lógica matemática, una cláusula de Horn es una cláusula (una disyunción de literales), con a lo sumo, uno positivo literal. Lleva ese nombre después que el lógico Alfred Horn, que fue el primero en señalar la importancia de estas cláusulas en 1951, en el artículo "On sentences which are true of direct unions of algebras".

Una cláusula de Horn con exactamente un literal positivo es una cláusula definitiva, una cláusula de Horn sin literales positivos a veces se denomina "cláusula de un objetivo",  sobre todo en la lógica de programación. Una fórmula de Horn es una forma normal conjuntiva cuyas cláusulas son todos de Horns, en otras palabras, se trata de una conjunción de  cláusulas de Horn. Un doble cláusula de Horn es una cláusula con a lo sumo, uno negativo literal. Las cláusulas de Horn vienen a desempeñar un papel fundamental en la lógica de 

programación. El siguiente es un ejemplo de una cláusula de Horn definitiva:

~ p V ~q V. . .  v ~t v u

Esta fórmula también puede ser escrita equivalentemente como una implicación:

(p^q^....^t) -> u