On automated theorem proving for assertional and refutational natural deduction systems

Abstract

Diese Arbeit befasst sich mit den Einsatz von Techniken der automatisierten Beweisführung (“automated theorem proving”, kurz ATP) im Bezug auf zwei Systeme des natürlichen Schließens für die klassische Aussagenlogik. Einerseits handelt es sich dabei um das weithin bekannte assertive Beweissystem nach Gentzen und Jaśkowski, andererseits um ein dazu komplementäres Verwerfungssystem nach Tamminga. Den Ansätzen folgend, die sich in der Literatur bei bereits existierenden ATPs für natürliches Schließen finden, erstellen wir zuerst eine Variante des Verwerfungssystems für die ein schwaches Normalisierungstheorem gilt, gefolgt von Varianten beider Systeme mit denen die Schleifenfreiheit der Beweise sichergestellt ist. Weiters implementieren und evaluieren wir Hermes, einen Prolog-ATP der parallel nach Assertions- und Verwerfungsbeweisen sucht. Aus unseren Beobachtungen geht hervor, dass sich mit einem solchen Programm durchaus Beweise generieren lassen, die den von Menschen erstellten ähneln, jedoch ist die Performanz insbesondere beim Generieren von Verwerfungsbeweisen nicht optimal, da gewisse gescheiterte Suchpfade intensives Backtracking erforderlich machen.

We investigate the use of automated theorem proving (ATP) techniques with regards to two natural deduction systems for classical propositional logic. One is the well-known assertional system following Gentzen and Jaśkowski, and the other is a refutational system due to Tamminga. Based on the approaches used by existing ATPs for natural deduction in the literature, we establish first a variant of the refutational system for which a weak normalisation theorem holds, and then variants of both systems that ensure loop-free derivations. We further implement and evaluate Hermes, a Prolog-based ATP that searches for assertional and refutational natural deduction derivations in parallel. Our observations show that this program is capable of producing remarkably human-like derivations for both valid and refutable formulas, but its performance, particularly in the refutational component, is not optimal due to the intensive backtracking required on certain failed derivation paths.