Forma
clausal:
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 implícitamente. 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
BIBLIOGRAFIA:
