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.
A terminating evaluation-driven variant of G3i / M. Ferrari, C. Fiorentini, G. Fiorino (LECTURE NOTES IN COMPUTER SCIENCE). - In: Automated Reasoning with Analytic Tableaux and Related Methods : 22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings / [a cura di] D. Galmiche, D. Larchey-Wendling. - Berlin : Springer, 2013. - ISBN 9783642405365. - pp. 104-118 (( Intervento presentato al 22. convegno International Conference tenutosi a Nancy nel 2013 [10.1007/978-3-642-40537-2_11].
A terminating evaluation-driven variant of G3i
C. Fiorentini;
2013
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
2013_tableaux.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
336.29 kB
Formato
Adobe PDF
|
336.29 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.