Eine Signatur ist eine Menge S mit
, S endlich oder abzählbar unendlich und
. Die Elemente von S heißen Atome oder atomare
Formeln. Eine atomare Formel hat die Form
(wobei ). Die
Menge der Wohlgeformten Formeln
wird durch folgenden induktiven Prozeß definiert:
Alle atomaren Formeln sind Formeln, d.h.
.
Für alle Formeln F und G sind
und Formeln (Konjunktion
und Disjunktion).
Für jede Formel F ist
eine Formel (Negation).
Folgende abkürzende Schreibweise ist gebräuchlich:
wird Implikation
genannt.
Definition 1.2: Literal
Ein Literal ist eine atomare Formel oder die Negation einer atomaren Formel
(positives bzw. negatives Literal).
Zur Vereinheitlichung von Schreibweisen für Formeln
verwendet man Normalformen. Zu jeder Formel gibt es äquivalente Formeln
in den unterschiedlichen Normalformen.
Definition 1.3: KNF
Eine Formel F ist in konjunktiver Normalform (KNF), falls sie eine
Konjunktion von Disjunktionen von Literalen ist:
wobei .
Definition 1.4: DNF
Eine Formel F ist in disjunktiver Normalform (DNF), falls sie eine
Disjunktion von Konjunktionen von Literalen ist:
wobei .
Satz 1.1: Normalformen
Für jede Formel F gibt es eine äquivalente Formel in KNF und
eine äquivalente Formel in DNF.
Definition 1.5: Klauseln
Formeln in KNF können als Mengen von KLauseln dargestellt werden:
Jedes Element der Menge F heißt Klausel. Die Elemente der
Klauseln sind Literale. Sie entsprechen den Disjunktionsgliedern der KNF.
Definition 1.6: Hornformel
F ist eine Hornformel (oder Hornklausel), falls F in KNF
ist und jedes Disjunktionsglied in F höchstens ein positives
Literal enthält.
Hornformeln können als Konjunktionen von Implikationen geschrieben
werden.
Das positive Literal einer Hornformel (oder Hornklausel) wird auch Klauselkopf,
die negativen Literale Klauselkörper
genannt.
Nicht jede Formel kann als Hornformel geschrieben werden, eine Hornformel
ist also keine Normalform.
Definition 1.7: Logisches
Programm
Ein logisches Programm besteht aus geoderten Klauseln.
, S endlich oder abzählbar unendlich und 
. Die Elemente von S heißen Atome oder atomare
Formeln. Eine atomare Formel hat die Form 
(wobei 
). Die
Menge der Wohlgeformten Formeln 
wird durch folgenden induktiven Prozeß definiert:
.
und 
Formeln (Konjunktion
und Disjunktion).
eine Formel (Negation).
.
wird