Horn's Clause

In propositional logic, a logical formula is a Horn clause if it is a (literal disjunction) clause with at most one positive literal. They are named after the logician Alfred Horn, who first pointed out the importance of these clauses in 1951.

This is an example of a Horn clause:

¬ ¬ p ¬ ¬ q ¬ ¬ t u{displaystyle neg plor neg qvee cdots vee neg tvee u}

A formula like this can also be equivalently rewritten as an implication:

(p∧ ∧ q∧ ∧ ∧ ∧ t)→ → u{displaystyle (pwedge qwedge cdots wedge t)rightarrow u}

A Horn clause with exactly one positive literal is a "definite" clause; in universal algebra the clauses "definites" they result (appear) as quasi-identities. A Horn clause without any positive literals is sometimes called a goal or a query clause, especially in logic programming.

A Horn formula is a textual string (string) of existential or universal quantifiers followed by a conjunction of Horn clauses.

Use in PROLOG

The syntax for a Horn clause in PROLOG looks like this:

 daughter(A,B) :- woman(A), father(B,A).

which could be read like this: "A is the daughter of B if A is a woman and B is the father of A".

In logical terms it represents the following implication:

(mujer(A)∧ ∧ padre(B,A))→ → hija(A,B){displaystyle (woman(A)land father(B,A))to hija(A,B)}

By definition of implication the following Horn clause is obtained:

¬ ¬ mujer(A) ¬ ¬ padre(B,A) hija(A,B){displaystyle lnot woman(A)lor lnot father(B,A)lor daughter(A,B)}

Note that, in PROLOG, the symbol :- separates the conclusion from the conditions. In PROLOG, variables are written starting with a capital letter. All conditions must be met simultaneously for the conclusion to be valid; therefore, the comma (in some versions of PROLOG the comma is replaced by the symbol &) that separates the different conditions is equivalent to the copulative conjunction.

In contrast, disjunction is not normally represented by special symbols (although it can be done with the ; symbol), but by adding new rules to the program. In this case:

 daughter(A,B) :- woman(A), father(B,A). daughter(A,B) :- woman(A), mother(B,A).

which could be read like this: "A is the daughter of B if A is a woman and B is the father of A or A is the daughter of B if A is a woman and B is the mother of A".