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 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 ).
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. 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 .