Previous: TR 89-04 Next: TR 90-01


Intellektik: Technical report 89-06

Die Konnektionsmethode

Gerd Neugebauer

Die logische Inferenz ist der Versuch, das rationale menschliche Denken zu formalisieren. Die Ansätze dazu reichen weit in der Geschichte zurück. Mit dem Aufkommen der Computer ist auch das Verlangen erwacht, das logische Schließen auch auf ihnen zu realisieren. Insbesondere wurden bekannte Verfahren dahingehend weiterentwickelt, daß sie auf den bekannten Computer-Architekturen geeignet abgearbeitet werden können. Die Ergebnisse dieser Bemühungen sind vor allem in dem Gebiet der Künstlichen Intelligenz zu sehen. Hier ist die logische Inferenz die Basis, auf der viele weitere Bemühungen beruhen. Die Konnektionsmethode ist eine Familie von Beweisverfahren, das auf den Arbeiten von W. Bibel basiert. Diese Arbeit soll einen Einblick in die grundlegenden Mechanismen der Konnektionsmethode verschaffen. Dabei lehnen wir uns weitgehend an die Vorgehensweise in \cite{bibel:atp} an. Diese Vorgehensweise ist die folgende. Zuerst werden anhand der Aussagenlogik die grundlegenden Begriffe eingeführt. Dies geschieht dadurch, daß Syntax und Semantik vollständig aus Mengen aufgebaut werden. Dazu kommt die ``klassische'' Schreibweise als Abkürzung für unübersichtliche Mengenausdrücke. Hier wird auch eine einfache Version der Konnektionsmethode vorgestellt. Daraufhin werden die Begriffe der Aussagenlogik so erweitert, daß die Prädikatenlogik erster Stufe behandelt werden kann. In analoger Vorgehensweise zu der Einführung der Aussagenlogik wird eine Konnektionsmethode für Prädikatenlogik erster Stufe aufgezeigt. Ein abschließender Abschnitt deutet neuere Tendenzen in der Forschung auf dem Gebiet der Konnektionsmethode an.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry