Article

Structural Cut Elimination

Author:

Frank PfenningAuthors Info & Claims

LICS '95: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science

Page 156

Published: 26 June 1995 Publication History

Publisher Site

Abstract

We present new proofs of cut elimination for intuitionistic, classical, and linear sequent calculi. In all cases the proofs proceed by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent derivations. This makes them amenable to elegant and concise implementations in Elf, a constraint logic programming language based on the LF logical framework.

Cited By

View all

Rocha PCaires L(2021)Propositions-as-types and shared stateProceedings of the ACM on Programming Languages10.1145/34735845:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473584
Rioux NZdancewic S(2020)Computation focusingProceedings of the ACM on Programming Languages10.1145/34089774:ICFP(1-27)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408977
Davies R(2017)A Temporal Logic Approach to Binding-Time AnalysisJournal of the ACM10.1145/301106964:1(1-45)Online publication date: 24-Mar-2017
https://dl.acm.org/doi/10.1145/3011069
Show More Cited By

Structural Cut Elimination
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
2. Mathematics of computing
  1. Continuous mathematics
    1. Calculus

Recommendations

Cut Elimination, Identity Elimination, and Interpolation in Super-Belnap Logics

We develop a Gentzen-style proof theory for super-Belnap logics (extensions of the four-valued Dunn---Belnap logic), expanding on an approach initiated by Pynko. We show that just like substructural logics may be understood proof-theoretically as logics ...
Cut Elimination for Monomial MALL Proof Nets
LICS '08: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science

We present a syntax for MALL (multiplicative additive linear logic without units) proof nets which refines Girard's one.It is also based on the use of monomial weights for identifying additive components (slices). Our generalization gives the ...
Eliminability of cut in hypersequent calculi for some modal logics of linear frames

Hypersequent calculus HC for three modal logics of linear frames (K4.3, KD4.3 and S4.3) is presented.Adequacy of HC for these logics is shown.Eliminability of Cut is demonstrated. Hypersequent calculi, introduced independently by Pottinger and Avron, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

LICS '95: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science

June 1995

ISBN:0818670506

Publisher

IEEE Computer Society

United States

Publication History

Published: 26 June 1995

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Rocha PCaires L(2021)Propositions-as-types and shared stateProceedings of the ACM on Programming Languages10.1145/34735845:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473584
Rioux NZdancewic S(2020)Computation focusingProceedings of the ACM on Programming Languages10.1145/34089774:ICFP(1-27)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408977
Davies R(2017)A Temporal Logic Approach to Binding-Time AnalysisJournal of the ACM10.1145/301106964:1(1-45)Online publication date: 24-Mar-2017
https://dl.acm.org/doi/10.1145/3011069
Miller DPimentel E(2013)A formal framework for specifying sequent calculus proof systemsTheoretical Computer Science10.5555/2438099.2438159474(98-116)Online publication date: 1-Feb-2013
https://dl.acm.org/doi/10.5555/2438099.2438159
Seo JPark S(2013)Judgmental subtyping systems with intersection types and modal typesActa Informatica10.1007/s00236-013-0186-250:7-8(359-380)Online publication date: 1-Dec-2013
https://dl.acm.org/doi/10.1007/s00236-013-0186-2
Lutovac TIvanović MBudimac Z(2012)An approach to automated reparation of failed proof attempts in propositional linear logic sequent calculusProceedings of the Fifth Balkan Conference in Informatics10.1145/2371316.2371329(64-69)Online publication date: 16-Sep-2012
https://dl.acm.org/doi/10.1145/2371316.2371329
Lam ECervesato IDe Schreye DJanssens GKing A(2012)Modeling datalog fact assertion and retraction in linear logicProceedings of the 14th symposium on Principles and practice of declarative programming10.1145/2370776.2370786(67-78)Online publication date: 19-Sep-2012
https://dl.acm.org/doi/10.1145/2370776.2370786
Dawson JGoré R(2010)Generic methods for formalising sequent calculi applied to provability logicProceedings of the 17th international conference on Logic for programming, artificial intelligence, and reasoning10.5555/1928380.1928399(263-277)Online publication date: 10-Oct-2010
https://dl.acm.org/doi/10.5555/1928380.1928399
Rabe FSchürmann CCheney JFelty A(2009)A practical module system for LFProceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice10.1145/1577824.1577831(40-48)Online publication date: 2-Aug-2009
https://dl.acm.org/doi/10.1145/1577824.1577831
Cervesato IScedrov A(2009)Relating state-based and process-based concurrency through linear logic (full-version)Information and Computation10.1016/j.ic.2008.11.006207:10(1044-1077)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.1016/j.ic.2008.11.006
Show More Cited By

Abstract

Cited By

Recommendations

Cut Elimination, Identity Elimination, and Interpolation in Super-Belnap Logics

Cut Elimination for Monomial MALL Proof Nets

Eliminability of cut in hypersequent calculi for some modal logics of linear frames

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations