gegeben, die wie folgt induktiv definiert ist:
Die klassische Aussagenlogik beschäftigt sich mit der Verknüpfung einfacher Ja-Nein-Aussagen durch Junktoren wie ,,Und”, ,,Oder”, ,,Nicht”etc.
Die Syntax aussagenlogischer Formeln ist durch die Menge gegeben, die wie folgt induktiv definiert ist:
;
;
, wenn 
;
, wenn 
und 
{∧,∨,⊂,⊃,↑,↓,⊅,⊄,≡,≢}.
Aussagenlogische Variablen und Konstanten werden auch als atomare aussagenlogische Formeln oder kurz Atome bezeichnet. Die Elemente der oben bereits erwähnten Menge {∧,∨,⊂,⊃,↑,↓,⊅,⊄,≡,≢}. heißen Junktoren, Konnektoren oder logische Operatoren.
Eine Funktion vom Typ
nennt man (aussagenlogische) Interpretation. Die Menge aller Interpretationen wird mit 
bezeichnet.
Diese Semantik aussagenlogischer Formeln wird durch eine Funktion
bestimmt. Diese 
ist wie folgt definiert:
für 
;
und
mit 
; für die Funktion
gilt:
,
, wobei die zum Junktor 
gehörende Funktion
wie in unten stehender Tabelle definiert ist.
Die folgende Tabelle gibt eine Übersicht über alle nicht-trivialen zweistelligen aussagenlogischen Funktionen:
Die Semantik aussagenlogischer Formeln wurde hier lediglich eingeführt, um nun den Begriff der Äquivalenz zweier aussagenlogischer Formeln formulieren. Dieser Begriff ist wesentlich für das vorliegende Programm, da die im nächsten Kapitel beschriebenen Normalformen stets äquivalent zur Ausgangsformel sein müssen. Zwei Formeln heißen äquivalent, wenn
für alle 
. Mit diesem Wissen ist es nun möglich, eine aussagenlogische Formel 
in eine andere aussagenlogische Formel 
umzuformen, wobei und äquivalent sind.
Paul Staroch