We present Gbu, a terminating variant of the sequent calculus G3i for ntuitionistic 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.
|Titolo:||A terminating evaluation-driven variant of G3i|
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
Settore MAT/01 - Logica Matematica
|Data di pubblicazione:||2013|
|Digital Object Identifier (DOI):||10.1007/978-3-642-40537-2_11|
|Tipologia:||Book Part (author)|
|Appare nelle tipologie:||03 - Contributo in volume|