A proof-search procedure for intuitionistic propositional logic
From MaRDI portal
Publication:377482
DOI10.1007/S00153-013-0342-YzbMATH Open1302.03034OpenAlexW2023242314MaRDI QIDQ377482FDOQ377482
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
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
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)
Cites Work
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Structural proof theory. With an appendix by Aarne Ranta
- Title not available (Why is that?)
- Title not available (Why is that?)
- On the intuitionistic force of classical search
- Connections in nonclassical logics
- Glivenko Classes of Sequents for Propositional Star-Free Likelihood Logic
- A Connection-Based Characterization of Bi-intuitionistic Validity
- Title not available (Why is that?)
Cited In (17)
- Long normal form proof search and counter-model generation
- Title not available (Why is that?)
- Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic
- Title not available (Why is that?)
- 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
- Intuitionistic Socratic procedures
- Proof finding algorithms for implicational logics
- Proof Search and Counter Model of Positive Minimal Predicate Logic
- Efficient SAT-based proof search in intuitionistic propositional logic
- Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
- SAT-based proof search in intermediate propositional logics
- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
Uses Software
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)
