Horn formula
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 .
definition
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.
Examples:

 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 
Satisfiability
With the help of the marking algorithm , Horn formulas can be tested in polynomial time for satisfiability (in addition, HORNSAT is Pcomplete ). 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 ).
application
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
literature
 HD Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic. BIWiss. Verlag, Mannheim / Leipzig / Vienna / Zurich 1992, ISBN 3411156031 .
 Wolfgang Rautenberg : Introduction to Mathematical Logic . 3. Edition. Vieweg + Teubner, Wiesbaden 2008, ISBN 9783834805782 .
 HansPeter Tuschik, Helmut Wolter: Mathematical logic  in short. Basics, model theory, decidability, set theory. BIWiss. Verlag, Mannheim / Leipzig / Vienna / Zurich 1994, ISBN 3411167319 .