Ein mehrsortiger Resolutionskalkül mit Paramodulation

Abstract

Der Resolutionskalkül mit Paramodulationsregel wird zu einem mehrsortigen Kalkül erweitert. Als Grundlage für das automatische Beweisen erhält man mit diesem Kalkül einen stark reduzierten Suchraum und einfachere Beweise. Die Vollständigkeit, die Korrektheit und der Sortensatz, der den neuen Kalkül mit seinem einsortigen Gegenstück in Beziehung setzt, werden bewiesen. Ergebnisse über Grundtermersetzungen und Unifikation in einem mehrsortigen Kalkül werden vorgestellt. Die Implementierung eines automatischen Beweisers für den neuen Kalkül wird beschrieben. Die Vorteile der Methode werden anhand ausgewählter Beispiele belegt.

The resolution calculus with paramodulationrule is extended to a many-sorted calculus. As a basis for Automated Theorem Proving, this many-sorted calculus leads to a remarkable reduction of the search space and also to simpler proofs. Soundness and completeness of the new calculus and the Sort-Theorem, which relates the many-sorted calculus to its one-sorted counterpart, are shown. In addition results about groundterm rewriting and unification in a many-sorted calculus are obtained. The practical consequences for an implementation of an automated theorem prover based on the many-sorted calculus are described. The advantages of the proposed method is verified by certain examples.