On the intuitionistic force of classical search

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

Eike Ritter, Lincoln Wallen, David J. Pym

Publication date: 23 August 2000

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

zbMATH Keywords

intuitionistic logic; \(\lambda\mu\)-calculus; classical proof-search; Harrop fragment; intuitionistic search; least-commitment principle; uniform proof

Mathematics Subject Classification ID

03B70: Logic in computer science

03B35: Mechanization of proofs and logical operations

03F03: Proof theory in general (including proof-theoretic semantics)

03B20: Subsystems of classical logic (including intuitionistic logic)

03B40: Combinatory logic and lambda calculus

Related Items

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

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