Some pitfalls of LK-to-LJ translations and how to avoid them

DOI10.1007/3-540-63104-6_14zbMath1430.03071OpenAlexW1584422534MaRDI QIDQ5234695

Uwe Egly

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_14

Mathematics Subject Classification ID

Structure of proofs (03F07)

Related Items (1)

On the intuitionistic force of classical search

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On different structure-preserving translations to normal form
• A structure-preserving clause form translation
• Intuitionistic propositional logic is polynomial-space complete
• Untersuchungen über das logische Schliessen. I
• On Glinvenko sequent classes
• Proof theory in the USSR 1925–1969
• On the intuitionistic force of classical search (Extended abstract)
• Proof-terms for classical and intuitionistic resolution
• Proof theory

This page was built for publication: Some pitfalls of LK-to-LJ translations and how to avoid them