Paper Info
Title
A Terminating Evaluation-Driven Variant of G3i.
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.
Year
DOI
Venue
2013
10.1007/978-3-642-40537-2_11
Lecture Notes in Artificial Intelligence
Field
DocType
Volume
Computer science,Sequent calculus,Algorithm,Propositional calculus,Sequent,Normalization property,Completeness (statistics),Calculus
Conference
8123
ISSN
Citations 
PageRank 
0302-9743
6
0.58
References 
Authors
6
3
Name
Order
Citations
PageRank
Mauro Ferrari19316.05
Camillo Fiorentini212121.00
Guido Fiorino39712.71