In
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
and
logic programming
Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...
, a Horn clause is a logical formula of a particular rule-like form which gives it useful properties for use in logic programming,
formal specification
In computer science, formal specifications are mathematically based techniques whose purpose are 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 verif ...
, and
model theory. Horn clauses are named for the logician
Alfred Horn
Alfred Horn (February 17, 1918 – April 16, 2001) was an American mathematician notable for his work in lattice theory and universal algebra. His 1951 paper "On sentences which are true of direct unions of algebras" described Horn claus ...
, who first pointed out their significance in 1951.
Definition
A Horn clause is a
clause (a
disjunction
In logic, disjunction is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is raining or it is snowing" can be represented in logic using the disjunctive formula R \lor S ...
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.
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:
All variables in a clause are implicitly
universally quantified
In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other ...
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
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems o ...
and
computational logic
Computational logic is the use of logic to perform or reason about computation. It bears a similar relationship to computer science and engineering as mathematical logic bears to mathematics and as philosophical logic bears to philosophy. It is s ...
. 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 ma ...
by
first-order resolution
In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically ...
, 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 if 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 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 usef ...
and solvable in
linear time.
Note that 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) is the problem of determining if there exists an interpretation that satisfie ...
is an
NP-complete
In computational complexity theory, a problem is NP-complete when:
# it is a problem for which the correctness of each solution can be verified quickly (namely, in polynomial time) and a brute-force search algorithm can find a solution by trying ...
problem.
Logic programming
Horn clauses are also the basis of
logic programming
Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...
, 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 SLD resolution (''Selective Linear Definite'' clause resolution) is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.
The SLD inference rule
Give ...
inference rule, used in implementation of the logic programming language
Prolog
Prolog is a logic programming language associated with artificial intelligence and computational linguistics.
Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...
.
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
Prolog is a logic programming language associated with artificial intelligence and computational linguistics.
Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...
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
Prolog is a logic programming language associated with artificial intelligence and computational linguistics.
Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...
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
In computer science, a universal Turing machine (UTM) is a Turing machine that can simulate an arbitrary Turing machine on arbitrary input. The universal machine essentially achieves this by reading both the description of the machine to be simu ...
.
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.
Notes
See also
*
Propositional calculus
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations ...
References
{{DEFAULTSORT:Horn clause
Logic in computer science
Normal forms (logic)