A Unified Procedure for Provability and Counter-Model Generation in Minimal Implicational Logic
- de Barros Santos, Jefferson
- Lopes Vieira, Bruno
- Haeusler, Edward Hermann
Publication date
September 2016
DOI Publisher
The Author(s). Published by Elsevier B.V.Abstract
AbstractThis paper presents results on the definition of a sequent calculus for Minimal Implicational Propositional Logic (M→) aimed to be used for provability and counter-model generation in this logic. The system tracks the attempts to construct a proof in such a way that, if the original formula is a M→ tautology, the tree structure produced by the proving process is a proof, otherwise, it is used to construct a counter-model using Kripke semantics
Add to ORKG