The a fortiori rule: the key to reach termination in intuitionistic logic
Giovanna Corsi · Archivio istituzionale della ricerca (Alma Mater Studiorum Università di Bologna) · 2006
We present a multi-succedent sequent calculus for the intuitionistic propositional logic which fulfils the subformula property and the termination property. A decision procedure is defined too so that for any formula either a proof in the given calculus or a counter-model is provided.