Horn Clause
   HOME

TheInfoList



OR:

In
mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
and
logic programming Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applyin ...
, 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 In computer science, formal specifications are mathematically based techniques whose purpose is to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verify ...
,
universal algebra Universal algebra (sometimes called general algebra) is the field of mathematics that studies algebraic structures in general, not specific types of algebraic structures. For instance, rather than considering groups or rings as the object of stud ...
and
model theory In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (mat ...
. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951.


Definition

A Horn clause is a disjunctive
clause In language, a clause is a Constituent (linguistics), constituent or Phrase (grammar), phrase that comprises a semantic predicand (expressed or not) and a semantic Predicate (grammar), predicate. A typical clause consists of a subject (grammar), ...
(a
disjunction In logic, disjunction (also known as logical disjunction, logical or, logical addition, or inclusive disjunction) is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is ...
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; a definite clause with no negative literals is a unit clause, and a unit clause without variables is a fact; 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: 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

Horn clauses play a basic role in constructive logic and computational logic. They are important in
automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...
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 In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations ...
. 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 In computational complexity theory, a decision problem is P-complete ( complete for the complexity class P) if it is in P and every problem in P can be reduced to it by an appropriate reduction. The notion of P-complete decision problems is use ...
and solvable in
linear time In theoretical computer science, the time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm. Time complexity is commonly estimated by counting the number of elementary operations ...
. In contrast, the unrestricted
Boolean satisfiability problem In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) asks whether there exists an Interpretation (logic), interpretation that Satisf ...
is an
NP-complete In computational complexity theory, NP-complete problems are the hardest of the problems to which ''solutions'' can be verified ''quickly''. Somewhat more precisely, a problem is NP-complete when: # It is a decision problem, meaning that for any ...
problem. In
universal algebra Universal algebra (sometimes called general algebra) is the field of mathematics that studies algebraic structures in general, not specific types of algebraic structures. For instance, rather than considering groups or rings as the object of stud ...
, 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. 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.


Logic programming

Horn clauses are also the basis of
logic programming Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applyin ...
, 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 SLD resolution (''Selective Linear Definite'' clause resolution) is the basic rule of inference, inference rule used in logic programming. It is a refinement of Resolution (logic), resolution, which is both Soundness, sound and refutation Completen ...
inference rule, used in implementation of the logic programming language
Prolog Prolog is a logic programming language that has its origins in artificial intelligence, automated theorem proving, and computational linguistics. Prolog has its roots in first-order logic, a formal logic. Unlike many other programming language ...
. 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 Prolog is a logic programming language that has its origins in artificial intelligence, automated theorem proving, and computational linguistics. Prolog has its roots in first-order logic, a formal logic. Unlike many other programming language ...
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 database A relational database (RDB) is a database based on the relational model of data, as proposed by E. F. Codd in 1970. A Relational Database Management System (RDBMS) is a type of database management system that stores data in a structured for ...
s, 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 In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformu ...
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.


See also

* Constrained Horn clauses *
Propositional calculus The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. Sometimes, it is called ''first-order'' propositional logic to contra ...


Notes


References

* * * * * * * * Logic in computer science Normal forms (logic) {{Normal forms in logic