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.

A Terminating Evaluation-Driven Variant of G3i

FERRARI, MAURO;
2013-01-01

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.
2013
D. Galmiche, D. Larchey-Wendling
Automated Reasoning with Analytic Tableaux and Related Methods
9783642405365
22nd International Conference, TABLEAUX 2013
Nancy, France
16-19 Settembre 2013
File in questo prodotto:
File Dimensione Formato  
g3ibu.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 164.13 kB
Formato Adobe PDF
164.13 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/2014120
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 6
social impact