Horn clause

(redirected from Horn clauses)

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 ?
The project proposes to examine the expressive power of higher-order Horn clauses by comparing them to other formalisms of verification.
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.
A sharp threshold for the phase transition of a restricted satisfiability problem for Horn clauses. J.
Once an axiom is completely written in the text box, it is parsed and transformed into Horn clauses through a skolemization process.
We show that when a clause set is order local, then the complexity of its ground entailment problem is a function of its structure (e.g., full versus Horn clauses), and the ordering used.
This subset is formed by Horn clauses [StSh86], which are (implicitly) universaly quantified, do not contain existencial quantifiers or functional symbols.
Finally, he proposed Guarded Horn Clauses (GHC) [22, 24].
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.
These include the standard Horn clauses and Krom clauses of propositional logic.
Starting from an extremely general and ambitious goal--the automatic proof of theorems in the full predicate calculus--researchers in the field were able to discover a meaningful related problem--that of proving theorems expressible by Horn clauses. (1) A thorough study of this related problem opened new vistas for attempting to tackle the difficult original problem of automating the formal methods envisioned by Frege in the late nineteenth century.
For example, the Horn clauses can include calls to attached procedures for numeric computations (for example, "distance(UofMD, BWI) [is less than] 50" in the previous example), or (in some of the implementations) any other procedure calls defined by the user.
The logic side of the debate has been definitively treated in [25], which eloquently sets forth the role of logic in the computational organization of knowledge and banishes the procedural-declarative dichotomy by insight that Horn clauses (that is, clause containing at most one unnegated literal) can be interpreted as procedures, and thus can be activated and executed by a suitably designed processor.