Horn clause

In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form that gives it useful properties for use in logic programming, formal specification, universal algebra and model theory. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951.[1]

Definition

A Horn clause is a disjunctive clause (a disjunction of literals) with at most one positive, i.e. unnegated, literal.

Conversely, a disjunction of literals with at most one negated literal is called a dual-Horn clause.

A Horn clause with exactly one positive literal is a definite clause or a strict Horn clause;[2] a definite clause with no negative literals is a unit clause,[3] and a unit clause without variables is a fact;[4]. A Horn clause without a positive literal is a goal clause. Note that the empty clause, consisting of no literals (which is equivalent to false) is a goal clause. These three kinds of Horn clauses are illustrated in the following propositional example:

Type of Horn clause Disjunction form Implication form Read intuitively as
Definite clause ¬p ∨ ¬q ∨ ... ∨ ¬t ∨ u u ← p ∧ q ∧ ... ∧ t assume that,
if p and q and ... and t all hold, then also u holds
Fact u u ← true assume that
u holds
Goal clause ¬p ∨ ¬q ∨ ... ∨ ¬t false ← p ∧ q ∧ ... ∧ t show that
p and q and ... and t all hold[note 1]

All variables in a clause are implicitly universally quantified with the scope being the entire clause. Thus, for example:

¬ human(X) ∨ mortal(X)

stands for:

∀X( ¬ human(X) ∨ mortal(X) ),

which is logically equivalent to:

∀X ( human(X) → mortal(X) ).

Significance

Horn clauses play a basic role in constructive logic and computational logic. They are important in automated theorem proving by first-order resolution, because the resolvent of two Horn clauses is itself a Horn clause, and the resolvent of a goal clause and a definite clause is a goal clause. These properties of Horn clauses can lead to greater efficiency of proving a theorem: the goal clause is the negation of this theorem; see Goal clause in the above table. Intuitively, if we wish to prove φ, we assume ¬φ (the goal) and check whether such assumption leads to a contradiction. If so, then φ must hold. This way, a mechanical proving tool needs to maintain only one set of formulas (assumptions), rather than two sets (assumptions and (sub)goals).

Propositional Horn clauses are also of interest in computational complexity. The problem of finding truth-value assignments to make a conjunction of propositional Horn clauses true is known as HORNSAT. This problem is P-complete and solvable in linear time.[5] Note that the unrestricted Boolean satisfiability problem is an NP-complete problem.

In universal algebra, definite Horn clauses are generally called quasi-identities; classes of algebras definable by a set of quasi-identities are called quasivarieties and enjoy some of the good properties of the more restrictive notion of a variety, i.e., an equational class.[6] From the model-theoretical point of view, Horn sentences are important since they are exactly (up to logical equivalence) those sentences preserved under reduced products; in particular, they are preserved under direct products. On the other hand, there are sentences that are not Horn but are nevertheless preserved under arbitrary direct products.[7]

Logic programming

Horn clauses are also the basis of logic programming, where it is common to write definite clauses in the form of an implication:

(p ∧ q ∧ ... ∧ t) → u

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 in implementation of the logic 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 reverse use of the clause, it is often written in the reverse form:

u ← (p ∧ q ∧ ... ∧ t)

In Prolog this is written as:

u :- p, q, ..., t.

In logic programming, computation and query evaluation are performed by representing the negation of a problem to be solved as a goal clause. For example, the problem of solving the existentially quantified conjunction of positive literals:

∃X (p ∧ q ∧ ... ∧ t)

is represented by negating the problem (denying that it has a solution), and representing it in the logically equivalent form of a goal clause:

∀X (false ← p ∧ q ∧ ... ∧ t)

In Prolog this is written as:

:- p, q, ..., t.

Solving the problem amounts to deriving a contradiction, which is represented by the empty clause (or "false"). The solution of the problem is a substitution of terms for the variables in the goal clause, which can be extracted from the proof of contradiction. Used in this way, goal clauses are similar to conjunctive queries in relational databases, and Horn clause logic is equivalent in computational power to a universal Turing machine.

The Prolog notation is actually ambiguous, and the term “goal clause” is sometimes also used ambiguously. The variables in a goal clause can be read as universally or existentially quantified, and deriving “false” can be interpreted either as deriving a contradiction or as deriving a successful solution of the problem to be solved.

Van Emden and Kowalski (1976) investigated the model-theoretic properties of Horn clauses in the context of logic programming, showing that every set of definite clauses D has a unique minimal model M. An atomic formula A is logically implied by D if and only if A is true in M. It follows that a problem P represented by an existentially quantified conjunction of positive literals is logically implied by D if and only if P is true in M. The minimal model semantics of Horn clauses is the basis for the stable model semantics of logic programs.[8]

Notes
  1. Like in resolution theorem proving, "show φ" and "assume ¬φ" are synonymous (indirect proof); they both correspond to the same formula, viz. ¬φ.

See also

References
  1. Horn, Alfred (1951). "On sentences which are true of direct unions of algebras". Journal of Symbolic Logic. 16 (1): 14–21. doi:10.2307/2268661. JSTOR 2268661. S2CID 42534337.
  2. Makowsky (1987). "Why Horn Formulas Matter in Computer Science: Initial Structures and Generic Examples" (PDF). Journal of Computer and System Sciences. 34 (2–3): 266–292. doi:10.1016/0022-0000(87)90027-4.
  3. Buss, Samuel R. (1998). "An Introduction to Proof Theory". In Samuel R. Buss (ed.). Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics. Vol. 137. Elsevier B.V. pp. 1–78. doi:10.1016/S0049-237X(98)80016-5. ISBN 978-0-444-89840-1. ISSN 0049-237X.
  4. Lau & Ornaghi (2004). "Specifying Compositional Units for Correct Program Development in Computational Logic". Program Development in Computational Logic. Lecture Notes in Computer Science. Vol. 3049. pp. 1–29. doi:10.1007/978-3-540-25951-0_1. ISBN 978-3-540-22152-4.
  5. Dowling, William F.; Gallier, Jean H. (1984). "Linear-time algorithms for testing the satisfiability of propositional Horn formulae". Journal of Logic Programming. 1 (3): 267–284. doi:10.1016/0743-1066(84)90014-1.
  6. Stanley Burris; H.P. Sankappanavar (1981). A Course in Universal Algebra. Springer-Verlag. ISBN 0-387-90578-2.
  7. Chang, Chen Chung; Keisler, H. Jerome (1990) [1973]. Model Theory. Studies in Logic and the Foundations of Mathematics (3rd ed.). Elsevier. ISBN 978-0-444-88054-3. Section 6.2
  8. van Emden, M. H.; Kowalski, R. A. (1976). "The semantics of predicate logic as a programming language" (PDF). Journal of the ACM. 23 (4): 733–742. CiteSeerX 10.1.1.64.9246. doi:10.1145/321978.321991. S2CID 11048276.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.