Clàusula de Horn

De Viquipèdia

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.