Das vorliegende Programm, der KNF-DNF-Konverter, ist ein interaktives, in Java geschriebenes Programm, welches im Rahmen eines Projektpraktikums bei Ao. Univ.Prof. Dr. Christian Fermüller an der Technischen Universität Wien entstanden ist. Es soll als Lehrbehelf für die Lehrveranstaltung Theoretische Informatik und Logik dienen. Die Funktion des Programms besteht in der Umformung einer beliebigen aussagenlogischen Formel in ihre äquivalente konjunktive Normalform (KNF) und disjunktive Normalform (DNF), wobei diese Umformung mit Hilfe der syntaktischen Methode erfolgen soll.
In dieser Dokumentation wird zunächst auf den theoretischen Hintergrund (,,Was ist eine aussagenlogische Formel?”, ,,Was versteht man unter der KNF/DNF?”) eingegangen. Im Anschluss daran wird das Programm beschrieben; einerseits dessen Bedienung und andererseits die innere Struktur - wie aussagenlogische Formeln in einer entsprechenden Datenstruktur abgelegt werden, wie die Umformung einer solchen Formel vor sich geht und wie Formeln vereinfacht werden.