<div class="csl-bib-body">
<div class="csl-entry">Maurer, M. (2022). <i>On automated theorem proving for assertional and refutational natural deduction systems</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.105603</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2023.105603
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/139691
-
dc.description.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.
de
dc.description.abstract
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.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
proof systems
en
dc.subject
automated deduction
en
dc.subject
automated theorem prover
en
dc.subject
natural deduction
en
dc.subject
refutation systems
en
dc.subject
complementary calculi
en
dc.title
On automated theorem proving for assertional and refutational natural deduction systems
en
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2023.105603
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Michael Maurer
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Diploma
-
dc.identifier.libraryid
AC16736878
-
dc.description.numberOfPages
110
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.advisor.orcid
0000-0001-5673-2460
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cf
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cf
-
item.fulltext
with Fulltext
-
item.grantfulltext
open
-
item.languageiso639-1
en
-
item.openairetype
Thesis
-
item.openairetype
Hochschulschrift
-
crisitem.author.dept
E194 - Institut für Information Systems Engineering