Tableau, Tableauresolution Und Tableaugraphresolution: Ein Neuer Weg Zur Automatischen Deduktion

Die Klauselresolution ist derzeit das popularste Deduktionsverfahren. Ihre Anwendung ist jedoch auf die Klauselmenge eingeschrankt. Die vorliegende Arbeit stellt ein Verfahren vor, das mit Hilfe von Unifikation bzw. Resolution die gesamte Pradikatenlogik bearbeitet. Die in dieser Arbeit eingefuhrten Tableaus - Polybaume mit Literaleinfarbung - dienen zur strukturisierten Formeldarstellung. Daraus erhalt man einen vollig neuen Kalkul, die Tableauresolution. Der Ubergang von der Tableauresolution zur Tableaugraphresolution erfolgt wie von der Klauselresolution zur Klauselgraphresolution. Systematisch werden die Eigenschaften wie Korrektheit, Vollstandigkeit und Konfluenz daruber ausgesprochen.