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

{\ displaystyle \ phi _ {1} \ vee \ phi _ {2} \ vee \ ldots \ vee \ phi _ {n}}

of literals , each being either an atomic expression (a positive literal) or the negation of such (a negative literal). ${\ displaystyle \ phi _ {i}}$

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:

{\ displaystyle \ neg p \ lor \ neg q \ vee \ ldots \ vee \ neg t \ vee u}

In this case, except for all atomic expressions (in this example they are propositional variables) are negations. ${\ displaystyle u}$

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

Examples:

${\ displaystyle (\ neg p \ vee \ neg q \ vee r) \ wedge (p \ vee \ neg q \ vee \ neg s) \ wedge (\ neg r \ vee \ neg s)}$
The third Horn clause has no, the other two Horn clauses each have a positive literal.
${\ displaystyle (x_ {1} \ vee \ neg x_ {2} \ vee \ neg x_ {3}) \ wedge (\ neg x_ {1} \ vee \ neg x_ {2} \ vee \ neg x_ {3} \ vee x_ {4})}$

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:

{\ displaystyle \ neg \ phi \ vee \ psi = \ phi \ Rightarrow \ psi}

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	${\ displaystyle \ neg x_ {1} \ vee \ ldots \ vee \ neg x_ {n}}$	${\ displaystyle x_ {1} \ wedge \ ldots \ wedge x_ {n} \ Rightarrow 0}$	${\ displaystyle x_ {1}, \ ldots, x_ {n}}$ are not all true
Definite Horn clause	Exactly one positive literal At least one negative literal	${\ displaystyle \ neg x_ {1} \ vee \ ldots \ vee \ neg x_ {n} \ vee y}$	${\ displaystyle x_ {1} \ wedge \ ldots \ wedge x_ {n} \ Rightarrow y}$	If are true, then is also true ${\ displaystyle x_ {1}, \ ldots, x_ {n}}$ ${\ displaystyle y}$
Factual clause	Exactly one positive literal No negative literal	${\ displaystyle y \! \;}$	${\ displaystyle 1 \ Rightarrow y}$	${\ displaystyle y \! \;}$ 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.

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 .