We present Gbu, a terminating variant of the sequent calculus G3i for intuitionistic propositional logic. Gbu modifies G3i by annotating the sequents so to distinguish rule applications into two phases: an unblocked phase where any rule can be backward applied, and a blocked phase where only right rules can be used. Derivations of Gbu have a trivial translation into G3i. Rules for right implication exploit an evaluation relation, defined on sequents; this is the key tool to avoid the generation of branches of infinite length in proof-search. To prove the completeness of Gbu, we introduce a refutation calculus Rbu for unprovability dual to Gbu. We provide a proof-search procedure that, given a sequent as input, returns either a Rbu-derivation or a Gbu-derivation of it
Ferrari, M., Fiorentini, C., Fiorino, G. (2013). A Terminating Evaluation-Driven Variant of G3i. In AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2013) (pp.104-118). SPRINGER [10.1007/978-3-642-40537-2_11].
A Terminating Evaluation-Driven Variant of G3i
FIORINO, GUIDO GIUSEPPE
2013
Abstract
We present Gbu, a terminating variant of the sequent calculus G3i for intuitionistic propositional logic. Gbu modifies G3i by annotating the sequents so to distinguish rule applications into two phases: an unblocked phase where any rule can be backward applied, and a blocked phase where only right rules can be used. Derivations of Gbu have a trivial translation into G3i. Rules for right implication exploit an evaluation relation, defined on sequents; this is the key tool to avoid the generation of branches of infinite length in proof-search. To prove the completeness of Gbu, we introduce a refutation calculus Rbu for unprovability dual to Gbu. We provide a proof-search procedure that, given a sequent as input, returns either a Rbu-derivation or a Gbu-derivation of it
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
