On the intuitionistic force of classical search (Extended abstract)

DOI10.1007/3-540-61208-4_19zbMath1415.03028OpenAlexW1587919740MaRDI QIDQ4645244

Lincoln Wallen, Eike Ritter, David J. Pym

Publication date: 10 January 2019

Published in: Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61208-4_19

zbMATH Keywords

sequent calculusnatural deductionintuitionistic logicclassical logicproof procedure

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Proof-terms for classical and intuitionistic resolution ⋮ On the semantics of classical disjunction ⋮ Some pitfalls of LK-to-LJ translations and how to avoid them ⋮ On the intuitionistic force of classical search

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• First-order modal tableaux
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• Untersuchungen über das logische Schliessen. II
• A note on the proof theory of the \(\lambda \Pi\)-calculus
• Uniform proofs as a foundation for logic programming
• The correspondence between cut-elimination and normalization
• A Uniform Proof-theoretic Investigation of Linear Logic Programming

This page was built for publication: On the intuitionistic force of classical search (Extended abstract)