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 existenciales o universales seguidos por una conjunción de 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.
En cambio la disyunción normalmente no se representa mediante símbolos especiales (aunque puede hacerse con el símbolo ;), sino añadiendo reglas nuevas al programa. En este caso:
cláusula, horn, este, artículo, sección, necesita, referencias, aparezcan, publicación, acreditada, este, aviso, puesto, noviembre, 2019, lógica, proposicional, fórmula, lógica, cláusula, horn, cláusula, disyunción, literales, como, máximo, literal, positivo, . Este articulo o seccion necesita referencias que aparezcan en una publicacion acreditada Este aviso fue puesto el 8 de noviembre de 2019 En logica proposicional una formula logica es una clausula de Horn si es una clausula disyuncion de literales con como maximo un literal positivo Se llaman asi por el logico Alfred Horn el primero en senalar la importancia de estas clausulas en 1951 Esto es un ejemplo de una clausula de Horn p q t u displaystyle neg p lor neg q vee cdots vee neg t vee u Una formula como esta tambien puede reescribirse de forma equivalente como una implicacion p q t u displaystyle p wedge q wedge cdots wedge t rightarrow u Una clausula de Horn con exactamente un literal positivo es una clausula definite en algebra universal las clausulas definites resultan aparecen como cuasi identidades Una clausula de Horn sin ningun literal positivo es a veces llamada clausula objetivo goal o consulta query especialmente en programacion logica Una formula de Horn es una cadena textual string de cuantificadores existenciales o universales seguidos por una conjuncion de clausulas de Horn Uso en PROLOG EditarLa sintaxis de una clausula de Horn en PROLOG tiene el siguiente aspecto hija A B mujer A padre B A que podria leerse asi A es hija de B si A es mujer y B es padre de A En terminos logicos representa la siguiente implicacion m u j e r A p a d r e B A h i j a A B displaystyle mujer A land padre B A to hija A B Por definicion de implicacion se obtiene la siguiente clausula de Horn m u j e r A p a d r e B A h i j a A B displaystyle lnot mujer A lor lnot padre B A lor hija A B Observese que en PROLOG el simbolo separa la conclusion de las condiciones En PROLOG las variables se escriben comenzando por una letra mayuscula Todas las condiciones deben cumplirse simultaneamente para que la conclusion sea valida por tanto la coma en algunas versiones de PROLOG se sustituye la coma por el simbolo amp que separa las distintas condiciones es equivalente a la conjuncion copulativa En cambio la disyuncion normalmente no se representa mediante simbolos especiales aunque puede hacerse con el simbolo sino anadiendo reglas nuevas al programa En este caso hija A B mujer A padre B A hija A B mujer A madre B A que podrian leerse asi A es hija de B si A es mujer y B es padre de A o A es hija de B si A es mujer y B es madre de A Vease tambien EditarProgramacion logica Programacion declarativa Alfred HornEnlaces externos EditarClausula de Horn en PlanetMath en ingles Datos Q933932Obtenido de https es wikipedia org w index php title Clausula de Horn amp oldid 136228326, wikipedia, wiki, leyendo, leer, libro, biblioteca,
