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

Volume:

2162

Date (published):

2018

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