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.
Corsi G. (2006). The a fortiori rule: the key to reach termination in intuitionistic logic. MILANO : Polimetrica.
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.
