Horn-Formel

Eine Horn-Klausel ist eine Darstellungsweise für Aussagen in der Aussagenlogik. Diese besteht aus einer Disjunktion von Literalen. Dabei ist höchstens ein Literal positiv.

Eine Horn-Klausel hat die Form:

$(\neg A_{1}\vee \dots \vee \neg A_{m}\vee C)$

Äquivalent dazu ist folgende Schreibweise:

$(A_{1}\vee \dots \vee A_{m})\rightarrow C$

Eine Konjunktion von Horn-Klauseln nennt man Horn-Form:

$B_{1}\wedge B_{2}\wedge \dots \wedge B_{n}$

Nicht jeder Aussage, die sich in der Aussagenlogik formulieren lässt, ist als Horn-Klausel darstellbar.

Die Bedeutung der Horn-Klauseln liegt z.B. in der Informatik beim maschinellen Schließen. Eine bekannte Programmiersprache mit Horn-Klauseln ist Prolog.