Clàusula de Horn
En lògica proposicional, una fórmula lògica és una clàusula de Horn si és una clàusula (disjunció de literals) amb, com a màxim, un literal positiu. Es diuen així pel lògic Alfred Horn, el primer a assenyalar la importància d'aquestes clàusules en 1951.[1]
Això és un exemple d'una clàusula de Horn:
Una fórmula com aquesta també pot reescriure's de forma equivalent com una implicació:
Una clàusula de Horn amb exactament un literal positiu és una clàusula "definite"; en àlgebra universal les clàusules "definites" resulten (apareixen) com quasi-identitats. Una clàusula de Horn sense cap literal positiu és de vegades anomeda clàusula objectiu (goal) o consulta (query), especialment en programació lògica.
Una fórmula de Horn és una cadena textual (string) de quantificadors existencials o universals seguits per una conjunció de clàusules de Horn.
Ús en PROLOG
La sintaxi d'una clàusula de Horn en PROLOG té el següent aspecte:
filla(A,B) :- dona(A), pare(B,A).
que podria llegir-se així: "A és filla de B si A és dona i B és pare de A".
En termes lògics representa la següent implicació:
Per definició d'implicació s'obté la següent clàusula de Horn:
Observe's que, en PROLOG, el símbol :- separa la conclusió de les condicions. En PROLOG, les variables s'escriuen començant per una lletra majúscula. Totes les condicions han de complir-se simultàniament perquè la conclusió siga vàlida; per tant, la coma (en algunes versions de PROLOG se substitueix la coma pel símbol &) que separa les diferents condicions és equivalent a la conjunció copulativa.
En canvi la disjunció normalment no es representa mitjançant símbols especials (encara que pot fer-se amb el símbol ;), sinó afegint regles noves al programa. En aquest cas:
filla(A,B) :- dona(A), pare(B,A). filla(A,B) :- dona(A), mare(B,A).
que podrien llegir-se així: "A és filla de B si A és dona i B és pare d'A o A és filla de B si A és dona i B és mare d'A".
Vegeu també
Enllaços externs
- Clàusula de Horn a PlanetMath (en anglés)
Referències
- ↑ Horn, Alfred «On sentences which are true of direct unions of algebras». Journal of Symbolic Logic, 16, 1951, pàg. 14–21. DOI: 10.2307/2268661. JSTOR: 2268661.