On the intuitionistic force of classical search

DOI10.1016/S0304-3975(99)00178-4zbMath0952.03007MaRDI QIDQ1575923

Lincoln Wallen, Eike Ritter, David J. Pym

Publication date: 23 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

intuitionistic logic\(\lambda\mu\)-calculusclassical proof-searchHarrop fragmentintuitionistic searchleast-commitment principleuniform proof

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items

A proof-search procedure for intuitionistic propositional logic ⋮ A short proof of the strong normalization of classical natural deduction with disjunction ⋮ On the semantics of classical disjunction ⋮ Non-strictly positive fixed points for classical natural deduction ⋮ Proof-search in type-theoretic languages: An introduction

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Forum: A multiple-conclusion specification logic
• First-order modal tableaux
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• Untersuchungen über das logische Schliessen. I
• 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
• Proof-terms for classical and intuitionistic resolution
• On the intuitionistic force of classical search (Extended abstract)
• The virtues of eta-expansion
• Some pitfalls of LK-to-LJ translations and how to avoid them