A proof-search procedure for intuitionistic propositional logic

DOI10.1007/S00153-013-0342-YMaRDI QIDQ377482zbMATHOpenAlexFDO

Publication date 6 November 2013

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00153-013-0342-y

sequent calculus Glivenko's theorem propositional intuitionistic logic

Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Structure of proofs (03F07) Complexity of proofs (03F20)

Recommendations

Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
On the intuitionistic force of classical search (extended abstract)
On sequent calculi for intuitionistic propositional logic.
scientific article; zbMATH DE number 1753197

Cites work

scientific article; zbMATH DE number 49746 (Why is no real title available?)
scientific article; zbMATH DE number 1497485 (Why is no real title available?)
scientific article; zbMATH DE number 3325541 (Why is no real title available?)
A connection-based characterization of bi-intuitionistic validity
Connections in nonclassical logics
Glivenko Classes of Sequents for Propositional Star-Free Likelihood Logic
On the intuitionistic force of classical search
Structural proof theory. With an appendix by Aarne Ranta
leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)

Cited in

(27)

Admissibility of structural rules for contraction-free systems of intuitionistic logic
Proof-search, analytic tableaux, models and counter-models, in hypo constructive semantics for minimal and intuitionistic propositional logic
A proof system for fork algebras and its applications to reasoning in logics based on intuitionism
Intuitionistic Socratic procedures
Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
Proof finding algorithms for implicational logics
Comparison of several proof systems of intuitionistic propositional logic
An evaluation-driven decision procedure for G3i
Efficient SAT-based proof search in intuitionistic propositional logic
Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
Proof-search in intuitionistic logic based on constraint satisfaction
Intuitionistic logic freed of all metarules
Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic
The logic of the weak excluded middle: A case study of proof-search
INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH
ADC method of proof search for intuitionistic propositional natural deduction
Proof Search and Counter Model of Positive Minimal Predicate Logic
scientific article; zbMATH DE number 1753197 (Why is no real title available?)
Long normal form proof search and counter-model generation
Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
On the intuitionistic force of classical search (extended abstract)
SAT-based proof search in intermediate propositional logics
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
A propositional system induced by Japaridze's approach to IF logic
On sequent calculi for intuitionistic propositional logic.
Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
scientific article; zbMATH DE number 4057508 (Why is no real title available?)

Describes a project that uses

Uses Software

leanCoP
ileanCoP
Pesca

This page was built for publication: A proof-search procedure for intuitionistic propositional logic

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