Community hub
Recent from talks
Contribute something
Nothing was collected or created yet.
Horn clause
View on WikipediaIn 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
[edit]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. 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[5] |
All variables in a clause are implicitly universally quantified with the scope being the entire clause. Thus, for example:
stands for:
which is logically equivalent to:
Significance
[edit]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.[6] In contrast, 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.[7] 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.[8]
Logic programming
[edit]Horn clauses are also the basis of logic programming, where it is common to write definite clauses in the form of an implication:
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 emphasize this reverse use of the clause, it is often written in the reverse form:
In Prolog this is written as:
u :- p, q, ..., t.
In logic programming, a goal clause, which has the logical form
represents the negation of a problem to be solved. The problem itself is an existentially quantified conjunction of positive literals:
The Prolog notation does not have explicit quantifiers and is written in the form:
:- p, q, ..., t.
This notation is ambiguous in the sense that it can be read either as a statement of the problem or as a statement of the denial of the problem. However, both readings are correct. In both cases, solving the problem amounts to deriving the empty clause. In Prolog notation this is equivalent to deriving:
:- true.
If the top-level goal clause is read as the denial of the problem, then the empty clause represents false and the proof of the empty clause is a refutation of the denial of the problem. If the top-level goal clause is read as the problem itself, then the empty clause represents true, and the proof of the empty clause is a proof that the problem has a solution.
The solution of the problem is a substitution of terms for the variables X in the top-level goal clause, which can be extracted from the resolution proof. 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.
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.[9]
See also
[edit]Notes
[edit]- ^ Horn 1951.
- ^ Makowsky 1987.
- ^ Buss 1998.
- ^ Lau & Ornaghi 2004.
- ^ Like in resolution theorem proving, "show φ" and "assume ¬φ" are synonymous (indirect proof); they both correspond to the same formula, viz. ¬φ.
- ^ Dowling & Gallier 1984.
- ^ Chang & Keisler 1990, Section 6.2.
- ^ van Emden & Kowalski 1976.
References
[edit]- Burris, Stanley; Sankappanavar, H.P., eds. (1981). A Course in Universal Algebra. Springer-Verlag. ISBN 0-387-90578-2.
- 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.
- 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.
- 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.
- 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.
- 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.
- Lau, Kung-Kiu; Ornaghi, Mario (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.
- Makowsky, J.A. (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.
Horn clause
View on GrokipediaFundamentals
Definition
A Horn clause is a clause in first-order logic, consisting of a disjunction of literals with at most one positive literal.[7] In the propositional case, this takes the syntactic form , where , each and is an atomic proposition, and may be absent, yielding the empty clause.[8] When and is present, the clause simplifies to the atomic fact ; when and is absent, it is the empty clause, often representing a contradiction or goal in proof procedures.[9] In first-order logic, Horn clauses are universally quantified, so the general form is , where is a tuple of variables, each and is an atomic formula, and the universal quantifiers are implicit in many contexts.[8] This structure is equivalent to the implication form , which underscores its interpretation as a rule: the conjunction of the positive antecedents implies the consequent.[9] Unlike a general clause, which permits any number of positive and negative literals in disjunctive form, a Horn clause restricts the positive literals to at most one; this limitation ensures the monotonicity of inference in Horn logic, where adding new facts cannot invalidate existing conclusions.[10] Horn clauses thus apply within the frameworks of both propositional logic and first-order logic, with variables and quantifiers appearing only in the latter under universal quantification.[7] The concept is named after the logician Alfred Horn, who introduced the relevant class of sentences in 1951 while studying their properties in the context of lattices and Boolean algebras, particularly their invariance under direct unions.[3]Examples
Horn clauses in propositional logic are disjunctions of literals containing at most one positive literal, often rewritten in implication form for clarity. A simple rule such as , equivalent to , represents the conditional "if then ."[11] A fact, which is a unit clause with a single positive literal like , asserts the truth of proposition without any conditions.[11] A goal clause, such as or equivalently , expresses a query about whether and can both be true, corresponding to the empty head in implication form.[11] In first-order logic, Horn clauses extend this form universally quantified over variables, with predicates replacing propositions. A definite clause like , or in disjunctive form , defines motherhood as a subset of parenthood for females.[12] Definite clauses have exactly one positive literal as the head, while goals are pure negative clauses without a head. Another example is , capturing the transitivity of parenthood.[12] Edge cases highlight special structures: the empty clause (or ) denotes falsehood and indicates unsatisfiability in a knowledge base.[11] Unit clauses, such as a single positive literal for a specific term, serve as unconditional facts. Pure negative clauses like act as constraints, forbidding certain combinations (e.g., no flying birds in this restrictive interpretation).[12] Natural language statements can be directly translated into Horn clauses for formal representation. For instance, "All birds fly" becomes , or disjunctively .[12]Theoretical Aspects
Properties
Horn clauses exhibit several key logical properties that distinguish them from more general forms of propositional or first-order logic. Sets of Horn clauses are closed under intersection in the lattice of formulas, meaning that the intersection of any collection of models of a Horn formula is itself a model; this property, established in Alfred Horn's seminal 1951 analysis of sentences true of direct unions of algebras, underpins the structural simplicity of Horn logic within Post lattices.[13][14] The satisfiability problem for Horn formulas, known as Horn-SAT, is P-complete, solvable in polynomial time through unit propagation, which iteratively resolves unit clauses (those with a single positive literal) until a contradiction or satisfaction is reached; this contrasts sharply with the NP-completeness of general SAT.[15][16] Every satisfiable Horn formula possesses a unique least Herbrand model, which is the smallest set of ground atoms closed under the formula's implications and serves as its canonical declarative semantics.[17] This least model can be computed constructively via forward chaining, applying the immediate consequence operator iteratively until a fixed point is reached.[18] Horn clause sets support complete inference procedures under restricted resolution strategies. Linear resolution is refutation-complete for Horn clauses, ensuring that any unsatisfiable set yields a refutation proof; for definite programs (sets of Horn clauses each with exactly one positive literal), the SLD-resolution variant provides both soundness and completeness with respect to the least Herbrand model.[19][20] The immediate consequence operator for Horn clauses is monotonic, preserving inclusions between interpretations (if one Herbrand interpretation is a subset of another, so is their image under the operator) and enabling the fixed-point semantics to converge to the least model while maintaining closure under conjunction and implication.[21]Significance
Horn clauses play a pivotal role in providing a computationally tractable fragment of first-order logic for key inference tasks, though full satisfiability remains undecidable as in general first-order logic, thereby facilitating efficient automated reasoning essential for knowledge representation systems. In propositional logic, the satisfiability problem for Horn clauses is solvable in polynomial time, enabling practical inference procedures like unit propagation and forward chaining that are complete for this class.[22] In the first-order setting, while general satisfiability remains semi-decidable, Horn clauses support monotonic inference through least-model semantics, allowing sound and complete deduction via bottom-up evaluation without the need for full resolution, which underpins their utility in representing and querying structured knowledge.[23] The theoretical foundations of Horn clauses trace back to Alfred Horn's 1951 analysis of sentences preserved under direct unions of algebras, particularly in the context of distributive lattices, where such sentences—now termed Horn sentences—characterize equational theories closed under products.[3] This work influenced subsequent developments in logic programming, notably through the application of fixed-point semantics to Horn clause programs, as formalized by van Emden and Kowalski in 1976, who drew on Dana Scott's 1970 framework for denotational semantics of programming languages to equate procedural execution with least fixed points.[24][25] These contributions established Horn clauses as a bridge between logical deduction and computational models, enabling declarative programming paradigms. In deductive databases, Horn clauses enable bottom-up computation via iterative fixed-point evaluation, as exemplified in Datalog, where programs converge to the least model representing all derivable facts from given rules and data.[24] This semantics supports scalable query answering over large datasets, contrasting with top-down approaches and forming the basis for relational database extensions. Despite their strengths, Horn clauses exhibit limitations in expressiveness, particularly for full negation, as they permit negative literals only in clause bodies and restrict heads to single positive atoms, precluding direct representation of disjunctive or negated conclusions without auxiliary constructs.[26] Such constraints are addressed in extensions like disjunctive Horn clauses, which generalize the form to allow multiple positive literals in heads for broader applicability. In contemporary contexts, Horn clauses underpin tractable subsets of description logics in the Semantic Web, such as the Horn fragment of ALC (Attributive Language with Complements), which ensures data complexity in AC0 and supports efficient reasoning in ontology languages like OWL 2 RL.[27]Applications
Logic Programming
Horn clauses form the foundational syntax of logic programming languages, particularly through the subset known as definite clause programs, where each clause consists of exactly one positive literal (the head) and any number of negative literals (the body). This structure allows programs to be expressed as a set of implications, where the head follows from the conjunction of the body literals being true. Definite clause programs enable declarative programming, in which the programmer specifies what is true rather than how to compute it, and the underlying inference engine handles the procedural aspects. The execution model for definite clause programs relies on SLD-resolution (Selective Linear Definite clause resolution), a variant of resolution that performs backward chaining to find substitutions that satisfy goals. In this process, the system starts with a goal (a set of literals to prove) and recursively matches it against clause heads, substituting variables to unify terms and then attempting to prove the corresponding body literals; it employs a depth-first search strategy with backtracking to explore alternative clauses when a branch fails. This mechanism implements a procedural interpretation of Horn clauses, transforming declarative rules into an executable search procedure. Robert Kowalski introduced this procedural view in 1972, emphasizing how Horn clauses could be interpreted as procedures for generating solutions, which laid the groundwork for logic programming as a computational paradigm. To extend Horn clauses beyond definite programs and handle negation in goals, logic programming incorporates negation as failure, which treats a literal as false if it cannot be proven true within a finite number of resolution steps. This approach, formalized in Keith Clark's completion theory in 1977, allows for non-Horn clauses by interpreting negation in terms of the program's logical completion, where unprovable atoms are assumed false under the closed world assumption. However, it introduces non-monotonic reasoning, limiting its expressiveness to stratified negation to avoid inconsistencies. Alain Colmerauer implemented these ideas in the first version of Prolog in 1972, making it the seminal logic programming language based on Horn clauses and enabling practical applications in areas like natural language processing. A representative example of a definite clause program is a simple ancestry query, where parent relationships are defined as Horn clauses and queried declaratively:parent(tom, bob).
parent(tom, liz).
parent(bob, ann).
parent(pat, bob).
parent(jim, pat).
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
parent(tom, bob).
parent(tom, liz).
parent(bob, ann).
parent(pat, bob).
parent(jim, pat).
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
?- ancestor(tom, ann). would succeed via SLD-resolution, unifying through the recursive clause to confirm tom as an ancestor of ann. This illustrates how Horn clauses enable concise, readable programs for relational queries without explicit control flow.