Tableau, Tableauresolution Und Tableaugraphresolution

Tableau, Tableauresolution Und Tableaugraphresolution Synopsis

Die Klauselresolution ist derzeit das populaerste Deduktionsverfahren. Ihre Anwendung ist jedoch auf die Klauselmenge eingeschraenkt. Die vorliegende Arbeit stellt ein Verfahren vor, das mit Hilfe von Unifikation bzw. Resolution die gesamte Praedikatenlogik bearbeitet. Die in dieser Arbeit eingefuehrten Tableaus - Polybaeume mit Literaleinfaerbung - dienen zur strukturisierten Formeldarstellung. Daraus erhaelt man einen voellig neuen Kalkuel, die Tableauresolution. Der Uebergang von der Tableauresolution zur Tableaugraphresolution erfolgt wie von der Klauselresolution zur Klauselgraphresolution. Systematisch werden die Eigenschaften wie Korrektheit, Vollstaendigkeit und Konfluenz darueber ausgesprochen.