Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-39465
Titel: | Ein mehrsortiger Resolutionskalkül mit Paramodulation |
VerfasserIn: | Walther, Christoph |
Sprache: | Deutsch |
Erscheinungsjahr: | 1984 |
Erscheinungsort: | Karlsruhe |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
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. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-394653 hdl:20.500.11880/35684 http://dx.doi.org/10.22028/D291-39465 |
Schriftenreihe: | Memo SEKI : SEKI-Projekt / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI |
Band: | 84,23 |
Datum des Eintrags: | 19-Apr-2023 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Professur: | SE - Sonstige |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
SEKI-MEMO-84-23_Walther_Ein-mehrsortiger-Resolutionskalkül-mit-Paramodulation.pdf | 62,99 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.