Efficient translation of sequent calculus proofs into natural deduction proofs

Ebner, Gabriel; Schlaipfer, Matthias

Record link:

https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3703
http://hdl.handle.net/20.500.12708/921

Title:

Efficient translation of sequent calculus proofs into natural deduction proofs

Citation:

Ebner, G., & Schlaipfer, M. (2018). Efficient translation of sequent calculus proofs into natural deduction proofs. In 6th Workshop on Practical Aspects of Automated Reasoning (PAAR) ; Konev, Boris; Urban, Josef; Rümmer, Philipp. PAAR 2018 Practical Aspects of Automated Reasoning, Oxford, United Kingdom of Great Britain and Northern Ireland (the). CEUR. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3703

CatalogPlus:

AC15131540

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Ebner, Gabriel
Schlaipfer, Matthias

Organisational Unit:

E191 - Institut für Informationssysteme

Published in:

Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018) : Oxford, UK, July 19th, 2018

Volume:

2162

Date (published):

2018

Event name:

PAAR 2018 Practical Aspects of Automated Reasoning

Event date:

19-Jul-2018

Event place:

Oxford, United Kingdom of Great Britain and Northern Ireland (the)

Number of Pages:

Publisher:

CEUR

Keywords:

Beweistheorie; Natürliches Schließen; Sequentenkalkül; Übersetzung

Proof theory; Natural deduction; Sequent calculus; Translation

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.

Additional information:

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>.

License:

In Copyright

Appears in Collections:

Conference Paper