A Unified Procedure for Provability and Counter-Model Generation in Minimal Implicational Logic
Jefferson de Barros Santos, Bruno Lopes Vieira, Edward Hermann Hæusler · Electronic Notes in Theoretical Computer Science · 2016
This 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.