Cláusula de Horn
cláusula (disyunción de literales) con, como máximo, un literal positivo / De Wikipedia, la enciclopedia encyclopedia
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.
Este artículo o sección necesita referencias que aparezcan en una publicación acreditada. |
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 existenciales o universales seguidos por una conjunción de cláusulas de Horn.