Vés al contingut

Clàusula de Horn

De la Viquipèdia, l'enciclopèdia lliure

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[modifica]

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é[modifica]

Enllaços externs[modifica]

Referències[modifica]

  1. 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.