A proof-search procedure for intuitionistic propositional logic

DOI10.1007/S00153-013-0342-YMaRDI QIDQ377482zbMATH OpenOpenAlexFDO

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)

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

Describes a project that uses

Uses Software

Pesca
ileanCoP
leanCoP

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)