Efficient translation of sequent calculus proofs into natural deduction proofs

Ebner, Gabriel; Schlaipfer, Matthias

Datensatz Zitierlink:

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

Titel:

Efficient translation of sequent calculus proofs into natural deduction proofs

Zitat:

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

Publikationstyp:

Konferenzbeitrag - Full-Paper Contribution

Sprache:

Englisch

Autor_innen:

Ebner, Gabriel
Schlaipfer, Matthias

Organisationseinheit:

E191 - Institut für Informationssysteme

Erschienen 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

Band:

2162

Datum (veröffentlicht):

2018

Veranstaltungsname:

PAAR 2018 Practical Aspects of Automated Reasoning

Veranstaltungszeitraum:

19-Jul-2018

Veranstaltungsort:

Oxford, Vereinigtes Königreich

Umfang:

Verlag:

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.

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

Lizenz:

Urheberrechtsschutz

Enthalten in den Sammlungen:

Conference Paper