A note on the complexity of classical and intuitionistic proofs

DOI10.1109/LICS.2015.66MaRDI QIDQ4635844zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cited in

(9)

• Some pitfalls of \textsf{LK}-to-\textsf{LJ} translations and how to avoid them
• 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
• scientific article; zbMATH DE number 65537 (Why is no real title available?)
• Algebraic proofs of cut elimination

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)