Theory Reasoning in Connection Calculi and the Linearizing Completion Approach

Diese Arbeit befaßt sich mit Erweiterungen von Kalkülen des Automatischen Theorembeweisens zum Theorieschließen. Im Mittelpunkt stehen Konnektionenmethoden, und dabei insbesondere die Theorie-Modell-Elimination (TME). Der Schwerpunkt bei TME liegt bei der Kombination mit Theorieschlußverfahren, die durch ein neuartiges Übersetzungsverfahren erhalten werden. Es werden mehrere Varianten von Konnektionen-basierten Theorieschluß-Kalkülen definiert und untereinander verglichen. Dabei wird TME als Basis für weitere Verfeinerungen ausgewählt. Die endgültigen Varianten sind Suchraumeingeschränkte Varianten der totalen TME, der Partiellen TME und der partiellen Restart-TME. Diese Varianten sind antwortvollständig und somit attraktiv als Basis für Logik-Programmierung und Problemlösungsanwendungen. Ein Theorieschluß-System ist nur funktionsfähig in der Kombination mit einem (effizienten) Hintergrund-Schlußverfahren immer neu von Hand zu entwerfen, schlage ich eine allgemeinere Methode vor, die ``linearisiende Vervollständigung'' (linearizing completion). Linearisiende Vervollständigung ermöglicht die automatische Konstruktion von Hintergrund-Schlußverfahren für TME-basierte Theorieschluß-Systeme. Die Methode ist anwendbar auf eine große Klasse von axiomatische gegebenen Theorien, nämlich Horn-Theorien. Technisch gesehen ermöglicht linearisierende Vervollständigung die Kombination der aus der Resolution bekannten Unit-Resulting Strategie mit einer zielorienten Strategie à la Prolog, und zwar auf eine widerlegungsvollständige Art und Weise. Die Methode wird im Detail vorgestellt. Schließlich wird eine Implementierung beschrieben, welch die PTTP-Technik (Prolog based Technology Theorem Probinv) geeignet zum Theorieschließen erweitert, und die Nützlichkeit der in dieser Arbeit beschriebenen Methoden wird experimentell nachgewiesen.