On the intuitionistic force of classical search (extended abstract)

DOI10.1007/3-540-61208-4_19MaRDI QIDQ4645244zbMATH OpenOpenAlexFDO

Authors Eike Ritter, Lincoln Wallen, David 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

classical logicintuitionistic logicnatural deductionproof proceduresequent calculus

Mathematics Subject Classification ID

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

Recommendations

• On the intuitionistic force of classical search
• scientific article; zbMATH DE number 1390270
• Proof-terms for classical and intuitionistic resolution
• A proof-search procedure for intuitionistic propositional logic
• Proof-Search in Natural Deduction Calculus for Classical Propositional Logic

Cites work

• A note on the proof theory of the -calculus
• A Uniform Proof-theoretic Investigation of Linear Logic Programming
• First-order modal tableaux
• scientific article; zbMATH DE number 4055570 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 65536 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 1348467 (Why is no real title available?)
• scientific article; zbMATH DE number 1478228 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3074068 (Why is no real title available?)
• The correspondence between cut-elimination and normalization
• The liberalized -rule in free variable semantic tableaux
• Uniform proofs as a foundation for logic programming
• Untersuchungen über das logische Schliessen. II

Cited in

(11)

• Proof-finding algorithms for classical and subclassical propositional logics
• On the intuitionistic force of classical search
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• Labelled proof systems for intuitionistic provability
• Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
• A proof-search procedure for intuitionistic propositional logic
• Proof-terms for classical and intuitionistic resolution
• scientific article; zbMATH DE number 1543301 (Why is no real title available?)
• Proof-terms for classical and intuitionistic resolution
• Some pitfalls of \textsf{LK}-to-\textsf{LJ} translations and how to avoid them
• On the semantics of classical disjunction

Describes a project that uses

Uses Software

• Automath

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4645244)