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

intuitionistic logicnatural deductionsequent calculusclassical logicproof procedure

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

• 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?)
• A Uniform Proof-theoretic Investigation of Linear Logic Programming
• A note on the proof theory of the -calculus
• First-order modal tableaux
• 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)

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

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)