Cláusula de Horn

En lógica proposicional, una fórmula lógica es una cláusula de Horn si es una cláusula (disyunción de literales) con, como máximo, un literal positivo. Se llaman así por el lógico Alfred Horn, el primero en señalar la importancia de estas cláusulas en 1951.

Esto es un ejemplo de una cláusula de Horn:

Una fórmula como esta también puede reescribirse de forma equivalente como una implicación:

Una cláusula de Horn con exactamente un literal positivo es una cláusula "definite"; en álgebra universal las cláusulas "definites" resultan (aparecen) como cuasi-identidades. Una cláusula de Horn sin ningún literal positivo es a veces llamada cláusula objetivo (goal) o consulta (query), especialmente en programación lógica.

Una fórmula de Horn es una cadena textual (string) de cuantificadores existentiales o universales seguidos por una conjunción nde cláusulas de Horn.


Uso en PROLOG

La sintaxis de una cláusula de Horn en PROLOG tiene el siguiente aspecto:

hija (A, B) :- mujer (A), padre (B, A).

que podría leerse así: "A es hija de B si A es mujer y B es padre de A".

En términos lógicos representa la siguiente implicación:

Por definición de implicación se obtiene la siguiente cláusula de Horn:

Obsérvese que, en PROLOG, el símbolo :- separa la conclusión de las condiciones. En PROLOG, las variables se escriben comenzando por una letra mayúscula. Todas las condiciones deben cumplirse simultáneamente para que la conclusión sea válida; por tanto, la coma (en algunas versiones de PROLOG se sustituye la coma por el símbolo &) que separa las distintas condiciones es equivalente a la conjunción copulativa.

La disyunción, en cambio, no se representa mediante símbolos especiales, sino definiendo reglas nuevas, como la siguiente:

hija (A, B) :- mujer (A), madre (B, A).

que podría leerse así: "A es hija de B si A es mujer y B es madre de A".

Other Languages
čeština: Hornova klauzule
Deutsch: Horn-Formel
English: Horn clause
français: Clause de Horn
magyar: Horn-klóz
日本語: ホーン節
қазақша: Хорн өрнегі
Nederlands: Horn-clausule
português: Cláusula de Horn
Simple English: Horn clause
српски / srpski: Хорнова клауза
українська: Диз'юнкт Горна
中文: 霍恩子句