To access the proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning, co-located with Federated Logic Conference 2018 (FLoC 2018), see URN: <a href="https://nbn-resolving.org/urn:nbn:de:0074-2162-4" target="_blank" >urn:nbn:de:0074-2162-4</a> or visit <a href=" http://ceur-ws.org/Vol-2162/" target="_blank">http://ceur-ws.org/Vol-2162/</a>.
-
dc.description.abstract
We present a simple and efficient translation of the classical multi-succedent sequent calculus LK to natural deduction. This translation aims to produce few excluded middle inferences, and to keep the quantifier complexity of the instances of excluded middle low. We evaluate the translation on proofs imported from resolution-based first-order theorem provers, and show that it achieves these goals in an efficient manner.
en
dc.description.sponsorship
Vienna Science and Technology Fund (WWTF)
-
dc.description.sponsorship
Austrian Science Fund (FWF)
-
dc.description.sponsorship
Austrian Science Fund (FWF)
-
dc.language
English
-
dc.language.iso
en
-
dc.publisher
CEUR
-
dc.relation.ispartofseries
CEUR Workshop Proceedings
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Beweistheorie
de
dc.subject
Natürliches Schließen
de
dc.subject
Sequentenkalkül
de
dc.subject
Übersetzung
de
dc.subject
Proof theory
en
dc.subject
Natural deduction
en
dc.subject
Sequent calculus
en
dc.subject
Translation
en
dc.title
Efficient translation of sequent calculus proofs into natural deduction proofs
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.relation.publication
6th Workshop on Practical Aspects of Automated Reasoning (PAAR) ; Konev, Boris; Urban, Josef; Rümmer, Philipp