Horn clause

(redirected from Horn clauses)

Horn clause

A set of atomic literals with at most one positive literal. Usually written

L <- L1, ..., Ln or <- L1, ..., Ln

where n>=0, "<-" means "is implied by" and comma stands for conjuction ("AND"). If L is false the clause is regarded as a goal. Horn clauses can express a subset of statements of first order logic.

The name "Horn Clause" comes from the logician Alfred Horn, who first pointed out the significance of such clauses in 1951, in the article "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21.

A definite clause is a Horn clause that has exactly one positive literal.
References in periodicals archive ?
This subset is formed by Horn clauses [StSh86], which are (implicitly) universaly quantified, do not contain existencial quantifiers or functional symbols.
The former metainterpreter works with a very reduced language as is with Horn clauses, that is, clauses with, at most, one positive literal (7) If A, [B.
The ordered resolution method is extremely efficient but can result to be not complete with languages composed of clauses that are not Horn clauses.