Horn clause


Also found in: Wikipedia.

Horn clause

(logic)
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 ?
Implication between a definite Horn formula [phi] and a definite Horn clause C can be decided by forward chaining: mark variables in the body of C and, while there is a clause in [phi] with all its body variables marked, mark its head variable as well.
n] [right arrow] s = t, is entailed by a Horn clause theory.
The mechanisms/functions of problem solving and inference that we have considered range from rather basic concepts such as list processing, pattern matching, chronological backtracking, and simple Horn clause deduction, to higher-level ones such as knowledge acquisition, inference by analogy, common sense reasoning, inductive inference, hypothetical reasoning, and metaknowledge deduction.
He pointed out that in view of the behavior of Horn clause linear-resolution proof-seeking processes, a collection of Horn clauses could be regarded as knowledge organized both declaratively and procedurally.
Prolog's power as a programming language comes from the fact that when SLD resolution is used as the evaluation technique, a Horn clause can be understood as defining a procedure (in the ordinary sense of procedural languages, e.
These specifications are written by constructing clauses that combine laws that use the Horn clause format described erlier.
However, for the purposes of efficient mechanical theorem proving only a subset of predicate calculus, Horn clause calculus, has as yet proved manageable.
With Ed Wilson and Roussel, I looked at both Horn clause and non-Horn clause definitions "executed" by SL-resolution.
Among the topics are free models for horn clauses over predicate fuzzy logics, a data mining methodology for event analysis in neurophysiological signals, using multi-agent systems to mediate in an assistive social network for the elder population, using kernal alignment for feature selection in schizophrenia diagnosis, and the domain adaptation problem in statistical machine translation systems.
Once an axiom is completely written in the text box, it is parsed and transformed into Horn clauses through a skolemization process.
This subset is formed by Horn clauses [StSh86], which are (implicitly) universaly quantified, do not contain existencial quantifiers or functional symbols.
Linear resolution is significant as the basis for the PROLOG programming language (where the format of the problem is restricted to Horn clauses, providing completeness for linear-input resolution) and its use in various high-performance ATP systems, for example, PTTP, PROTEIN, and METEOR.