A note on the complexity of classical and intuitionistic proofs

DOI10.1109/LICS.2015.66zbMATH Open1395.03027OpenAlexW2141291205MaRDI QIDQ4635844FDOQ4635844

Authors: Matthias Baaz, Alexander Leitsch, Giselle Reis 

Publication date: 23 April 2018

Published in: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/lics.2015.66

Recommendations

• Algebraic proofs of cut elimination
• Some pitfalls of \textsf{LK}-to-\textsf{LJ} translations and how to avoid them
• Bounds for cut elimination in intuitionistic propositional logic
• Publication:3475264
• Cut-elimination and redundancy-elimination by resolution

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Cited In (9)

• A generalization of a conservativity theorem for classical versus intuitionistic arithmetic
• Glivenko sequent classes in the light of structural proof theory
• Almost all Classical Theorems are Intuitionistic
• Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk)
• Exploring Computational Contents of Intuitionist Proofs
• Correspondences between classical, intuitionistic and uniform provability
• Title not available (Why is that?)
• Algebraic proofs of cut elimination
• Some pitfalls of \textsf{LK}-to-\textsf{LJ} translations and how to avoid them

This page was built for publication: A note on the complexity of classical and intuitionistic proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635844)