A unified procedure for provability and counter-model generation in minimal implicational logic

DOI10.1016/J.ENTCS.2016.09.014MaRDI QIDQ2397231zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

theorem proving

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

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

Cites work

• scientific article; zbMATH DE number 1189111 (Why is no real title available?)
• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• scientific article; zbMATH DE number 895271 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• A new algorithm for derivability in the constructive propositional calculus
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• Contraction-free sequent calculi for intuitionistic logic
• Efficient loop-check for backward proof search in some non-classical propositional logics
• Eigenvariables, bracketing and the decidability of positive minimal predicate logic
• Focusing and Polarization in Intuitionistic Logic
• How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning
• Logic Programming with Focusing Proofs in Linear Logic
• Logical Approaches to Computational Barriers
• Propositional logics complexity and the sub-formula property
• Two loop detection mechanisms: a comparison

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)