In mathematical logic, a Horn clause is a clause (a disjunction of literals) with at most one positive literal. They are named after 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 Horn clause with exactly one positive literal is a definite clause; in universal algebra definite clauses appear as quasiidentities. A Horn clause with no positive literals is sometimes called a goal clause or query clause, especially in logic programming. A Horn formula is a conjunction of Horn clauses; that is, a conjunctive normal form formula whose clauses are all Horn. A dual-Horn clause is a clause with at most one negative literal. Horn clauses play a basic role in logic programming and are important for constructive logic.
The following is an example of a (definite) Horn clause:
Such a formula can also be written equivalently in the form of an implication:
Horn clauses can be propositional or first order, depending on whether we consider propositional or first-order literals.
The relevance of Horn clauses to theorem proving by first-order resolution is that the resolution of two Horn clauses is a Horn clause. Moreover, the resolution of a goal clause and a definite clause is again a goal clause. In automated theorem proving, this can lead to greater efficiencies in proving a theorem (represented as a goal clause).
In fact, the resolution of a goal clause with a definite clause to produce a new goal clause is the basis of the SLD resolution inference rule, used to implement logic programming and the programming language Prolog. In logic programming a definite clause behaves as a goal-reduction procedure. For example, the Horn clause written above behaves as the procedure:
- to show u, show p and show q and
and show t.
To emphasize this backwards use of the clause, it is often written using the consequence operator:
This is written in Prolog as follows:
u :- p, q, ..., t.
Propositional Horn clauses are also of interest in computational complexity, where the problem of finding a set of variable assignments to make a conjunction of Horn clauses true is a P-complete problem, sometimes called HORNSAT. This is P's version of the boolean satisfiability problem, a central NP-complete problem. Satisfiability of first-order Horn clauses is undecidable.
Bibliography
- Alfred Horn, (1951) "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21.
External links
- Alex Sakharov, Horn Clause at MathWorld.
This article was originally based on material from the Free On-line Dictionary of Computing, which is licensed under the GFDL.
This entry is from Wikipedia, the leading user-contributed encyclopedia. It may not have been reviewed by professional editors (see full disclaimer)
