<div class="csl-bib-body">
<div class="csl-entry">Ciabattoni, A., Lang, T. A., & Ramanayake, D. R. S. (2023). Cut-Restriction: From Cuts to Analytic Cuts. In <i>2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)</i> (pp. 1–13). IEEE. https://doi.org/10.1109/LICS56636.2023.10175785</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/190611
-
dc.description.abstract
Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations into decidability, complexity, disjunction property, interpolation, and more. Unfortunately cut-elimination does not hold for the sequent calculi of most non-classical logics. It is well-known that the key to applications is the subformula property (a typical consequence of cut-elimination) rather than cut-elimination itself. With this in mind, we introduce cut-restriction, a procedure to restrict arbitrary cuts to analytic cuts (when elimination is not possible). The algorithm applies to all sequent calculi satisfying language-independent and simple-to-check conditions, and it is obtained by adapting age-old cut-elimination. Our work encompasses existing results in a uniform way, subsumes Gentzen's cut-elimination, and establishes new analytic cut properties.
en
dc.language.iso
en
-
dc.subject
Cut-elimination
en
dc.subject
proof theory
en
dc.subject
subformula property
en
dc.subject
sequent calculus
en
dc.subject
bi-intuitionistic logic
en
dc.title
Cut-Restriction: From Cuts to Analytic Cuts
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.relation.isbn
9798350335873
-
dc.description.startpage
1
-
dc.description.endpage
13
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
-
tuw.peerreviewed
true
-
tuw.relation.publisher
IEEE
-
tuw.relation.publisherplace
Piscataway
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Computer Science Foundations
-
tuw.researchTopic.value
100
-
tuw.linking
https://ieeexplore.ieee.org/document/10175826
-
tuw.linking
https://doi.org/10.1109/LICS56636.2023.10175785
-
tuw.publication.orgunit
E192-05 - Forschungsbereich Theory and Logic
-
tuw.publisher.doi
10.1109/LICS56636.2023.10175785
-
dc.description.numberOfPages
13
-
tuw.author.orcid
0000-0002-7940-9065
-
tuw.event.name
2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
-
tuw.event.startdate
26-06-2023
-
tuw.event.enddate
29-06-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Boston, MA
-
tuw.event.country
US
-
tuw.event.presenter
Ciabattoni, Agata
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.fulltext
no Fulltext
-
item.grantfulltext
restricted
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
crisitem.author.dept
E192-05 - Forschungsbereich Theory and Logic
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering