Horn formula

from Wikipedia, the free encyclopedia

Horn formulas are an important type of predicate logic formula. They play a central role in logical programming and are important for constructive logic. They were named after the American mathematician Alfred Horn .


A clause, also known as a disjunction term , is the disjunction

of literals , each being either an atomic expression (a positive literal) or the negation of such (a negative literal).

A Horn clause is a clause with at most one positive literal; H. with at most one literal that is not a negation.

In the special case of propositional logic, a typical Horn clause looks like this:

In this case, except for all atomic expressions (in this example they are propositional variables) are negations.

A Horn formula is a conjunctive normal form (that is, a conjunction of disjunctions) in which each disjunction term is a Horn clause.


  • The third Horn clause has no, the other two Horn clauses each have a positive literal.

Forms of representation of Horn clauses

Horn clauses can also be represented as material implications according to the rules of propositional logic . In the simplest case of a Horn clause with two literals, it is known that:

By definition, a Horn clause can contain exactly one or no positive literal (i.e. at most one atomic expression). It can also happen that there are no negations at all among the literals. There are therefore three basic types of Horn clauses. The following table gives an overview of these three possible forms of a Horn clause, both as a disjunction and as an implication.

Surname description Disjunction implication In words
Target clause No positive literal
At least one negative literal
are not all true
Definite Horn clause Exactly one positive literal
At least one negative literal
If are true, then is also true
Factual clause Exactly one positive literal
No negative literal
is true


With the help of the marking algorithm , Horn formulas can be tested in polynomial time for satisfiability (in addition, HORNSAT is P-complete ). So you can determine in polynomial time whether a variable assignment (an assignment of truth values ​​to the literals occurring in the Horn formula) exists for which the Horn formula becomes true. In contrast to this, it is assumed that there is generally no polynomial time algorithm for propositional logic formulas (see the satisfiability problem of propositional logic ).


The importance of the Horn clauses is in the computer science in mechanical Close . So in are programming language Prolog programs specified as Horn clauses.

See also


  • HD Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic. BI-Wiss. Verlag, Mannheim / Leipzig / Vienna / Zurich 1992, ISBN 3-411-15603-1 .
  • Wolfgang Rautenberg : Introduction to Mathematical Logic . 3. Edition. Vieweg + Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2 .
  • Hans-Peter Tuschik, Helmut Wolter: Mathematical logic - in short. Basics, model theory, decidability, set theory. BI-Wiss. Verlag, Mannheim / Leipzig / Vienna / Zurich 1994, ISBN 3-411-16731-9 .