Horn-Logik

Zusammenfassung

Wie wir bisher gesehen haben, ist das Schlußfolgern in der Aussagenlogik — selbst wenn wir Formeln in Konjunktiver Normalform betrachten — im schlechtesten Fall eine aufwendige und komplexe Angelegenheit. Es stellt sich ganz natürlich die Frage nach Teilklassen der Aussagenlogik, die noch eine vernünftige, d.h. nicht-triviale Ausdruckskraft besitzen, aber eine schnelle Bearbeitung zulassen. Eine solche Teilklasse wollen wir in diesem Kapitel betrachten. Sie ist nach A. Horn benannt, der sich zuerst mit diesen Formeln (für die Prädikatenlogik) beschäftigt hat. Die Klasse der Horn-Formeln um-faßt alle Formeln in Konjunktiver Normalform, deren Klauseln sich als Implikationen zwischen positiven Literalen als Prämisse und (maximal) einem positiven Literal als Konklusion darstellen lassen. Diese recht übersichtliche Form von „wenn-dann-Aussagen“ kann sicherlich als ein Grund für den erfolgreichen Einsatz von Wissensrepräsentationen angesehen werden, die auf Horn-Formeln basieren.