DC Field
Value
Language
dc.contributor.author
Ebner, Gabriel
-
dc.contributor.author
Schlaipfer, Matthias
-
dc.date.accessioned
2020-06-27T18:26:38Z
-
dc.date.issued
2018
-
dc.identifier.citation
<div class="csl-bib-body"> <div class="csl-entry">Ebner, G., &#38; Schlaipfer, M. (2018). Efficient translation of sequent calculus proofs into natural deduction proofs. In <i>6th Workshop on Practical Aspects of Automated Reasoning (PAAR) ; Konev, Boris; Urban, Josef; Rümmer, Philipp</i>. 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</div> </div>
-
dc.identifier.uri
https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3703
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/921
-
dc.description
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
-
dc.relation.issn
1613-0073
-
dc.relation.grantno
VRG12-004
-
dc.relation.grantno
S11403-N23
-
dc.relation.grantno
W1255-N23
-
dc.rights.holder
Copyright © 2018 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors.
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
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
-
tuw.container.volume
2162
-
tuw.relation.publisherplace
Oxford, UK
-
tuw.version
vor
-
tuw.publication.orgunit
E191 - Institut für Informationssysteme
-
dc.identifier.libraryid
AC15131540
-
dc.description.numberOfPages
17
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:3-3703
-
dc.rights.identifier
Urheberrechtsschutz
de
dc.rights.identifier
In Copyright
en
tuw.event.name
PAAR 2018 Practical Aspects of Automated Reasoning
-
tuw.event.startdate
19-07-2018
-
tuw.event.enddate
19-07-2018
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Oxford
-
tuw.event.country
GB
-
tuw.event.presenter
Ebner, Gabriel
-
item.grantfulltext
open
-
item.openairetype
conference paper
-
item.fulltext
with Fulltext
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E104-02 - Forschungsbereich Computational Logic
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.parentorg
E104 - Institut für Diskrete Mathematik und Geometrie
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
Appears in Collections:
Conference Paper
Thumbnail
Ebner Gabriel - 2018 - Efficient translation of sequent calculus proofs into...pdf
Adobe PDF
(386.64 kB)
Open Access
Show simple item record

Page view(s)

395
checked on Nov 20, 2023

Download(s)

104
checked on Nov 20, 2023

Google ScholarTM

Check