created: 2018-04-15 12:58:40 (+00:00; UTC; UTC)
last modified: 2018-04-22 14:04:26 (+00:00; UTC; UTC)
Diese Arbeit ist eine Machbarkeitsstudie, welche untersucht, inwieweit die Paramodulation in einem Deduktionstool realisierbar ist. Wenn sie realisierbar ist, soll ein solches Tool implementiert werden, dass die Paramodulation unterstützt. Das Ergebnis der Studie ist, dass die Paramodulation in einem Deduktionstool mit Einschränkungen realisierbar ist. In der Arbeit werden die logischen Grundlagen für die Deduktion vorgestellt. Es wird weiterhin die Paramodulationsregel definiert und gezeigt, dass sie die Gleichheitsaxiome erfüllt. Zwei eingeschränkte Varianten der Paramodulationen werden vorgestellt: die geordnete und die gerichtete Paramodulation. Für das Deduktionstool werden Algorithmen für die Komposition von Termersetzungen und für die Unifikation gezeigt. Zur einfachen Erweiterung des Tools werden Plug-ins verwendet. Als Optimierungen werden die Eliminierung von Teilzielen und die Speicherung der Hypothese bereits erreichter Ziele (für eine Erkennung von unendlichen Schleifen) eingesetzt. Weiterhin wird die Syntax der Paramodulation im Deduktionstool und die Einordnung der Paramodulation in den Kontrollfluss des Tools beschrieben. Bei der Implementierung der Paramodulationsregel sind Probleme aufgetreten. Deren Lösungen und die daraus entstandenen Einschränkungen werden beschrieben.