A unified procedure for provability and counter-model generation in minimal implicational logic
DOI10.1016/J.ENTCS.2016.09.014zbMATH Open1396.03013OpenAlexW2528753172WikidataQ113317659 ScholiaQ113317659MaRDI QIDQ2397231FDOQ2397231
Authors: Jefferson de Barros Santos, Bruno Lopes Vieira, Edward Hermann Haeusler 
Publication date: 19 May 2017
Full work available at URL: https://doi.org/10.1016/j.entcs.2016.09.014
Recommendations
- Proof Search and Counter Model of Positive Minimal Predicate Logic
- Proof-search, analytic tableaux, models and counter-models, in hypo constructive semantics for minimal and intuitionistic propositional logic
- Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
- \textsc{Minlog}: a minimal logic theorem prover
- Long normal form proof search and counter-model generation
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)
Cites Work
- Title not available (Why is that?)
- Logic Programming with Focusing Proofs in Linear Logic
- Efficient loop-check for backward proof search in some non-classical propositional logics
- Title not available (Why is that?)
- Propositional logics complexity and the sub-formula property
- Contraction-free sequent calculi for intuitionistic logic
- Eigenvariables, bracketing and the decidability of positive minimal predicate logic
- Focusing and Polarization in Intuitionistic Logic
- Logical Approaches to Computational Barriers
- An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
- Title not available (Why is that?)
- Two loop detection mechanisms: a comparison
- A new algorithm for derivability in the constructive propositional calculus
- Title not available (Why is that?)
- Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
- How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning
Cited In (5)
- Minimal models vs. logic programming: the case of counterfactual conditionals
- Proof Search and Counter Model of Positive Minimal Predicate Logic
- Proof-search, analytic tableaux, models and counter-models, in hypo constructive semantics for minimal and intuitionistic propositional logic
- CSymLean: A Theorem Prover for the Logic CSL over Symmetric Minspaces
- The existential fragment of second-order propositional intuitionistic logic is undecidable
This page was built for publication: A unified procedure for provability and counter-model generation in minimal implicational logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2397231)
