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.
The a fortiori rule: the key to reach termination in intuitionistic logic / Corsi G.. - STAMPA. - (2006), pp. 27-47.
The a fortiori rule: the key to reach termination in intuitionistic logic
CORSI, GIOVANNA
2006
Abstract
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.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.