It is well known that G3i, the sequent calculus for intuitionistic propositional logic where weakening and contraction are absorbed into the rules, is not terminating. Indeed, due to the contraction in the rule for left implication, the naïve goal-oriented proof-search strategy, consisting in applying the rules of the calculus bottom up until possible, can generate branches of infinite length. The usual solution to this problem is to support the proof-search procedure with a loop checking mechanism that prevents the generation of infinite branches by storing and analyzing some information regarding the branch under development. In this article, we propose a new technique based on evaluation functions. An evaluation function is a lightweight computational mechanism that, analyzing only the current goal of the proof search, allows one to drive the application of rules to guarantee termination and to avoid useless backtracking. We describe an evaluation-driven proof-search procedure that given a sequent σ returns either a G3i-derivation of σ or a countermodel for σ. We prove that such a procedure is terminating and correct, and that the depth of the G3i-trees generated during proof search is quadratic in the size of σ. Finally, we discuss the overhead time introduced by evaluation functions in the proof-search procedure.

Ferrari, M., Fiorentini, C., & Fiorino, G. (2015). An evaluation-driven decision procedure for G3i. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 16(1), 1-37 [10.1145/2660770].

An evaluation-driven decision procedure for G3i

FIORINO, GUIDO GIUSEPPE
Ultimo
2015

Abstract

It is well known that G3i, the sequent calculus for intuitionistic propositional logic where weakening and contraction are absorbed into the rules, is not terminating. Indeed, due to the contraction in the rule for left implication, the naïve goal-oriented proof-search strategy, consisting in applying the rules of the calculus bottom up until possible, can generate branches of infinite length. The usual solution to this problem is to support the proof-search procedure with a loop checking mechanism that prevents the generation of infinite branches by storing and analyzing some information regarding the branch under development. In this article, we propose a new technique based on evaluation functions. An evaluation function is a lightweight computational mechanism that, analyzing only the current goal of the proof search, allows one to drive the application of rules to guarantee termination and to avoid useless backtracking. We describe an evaluation-driven proof-search procedure that given a sequent σ returns either a G3i-derivation of σ or a countermodel for σ. We prove that such a procedure is terminating and correct, and that the depth of the G3i-trees generated during proof search is quadratic in the size of σ. Finally, we discuss the overhead time introduced by evaluation functions in the proof-search procedure.
Articolo in rivista - Articolo scientifico
Scientifica
Intuitionistic propositional logic; Proof-search procedures; Sequent calculi;
Intuitionistic propositional logic; Proof-search procedures; Sequent calculi; Computer Science (all); Theoretical Computer Science; Computational Mathematics; Logic
English
Ferrari, M., Fiorentini, C., & Fiorino, G. (2015). An evaluation-driven decision procedure for G3i. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 16(1), 1-37 [10.1145/2660770].
Ferrari, M; Fiorentini, C; Fiorino, G
File in questo prodotto:
File Dimensione Formato  
FIORINO-TOCL-2015.pdf

Solo gestori archivio

Tipologia di allegato: Publisher’s Version (Version of Record, VoR)
Dimensione 760.16 kB
Formato Adobe PDF
760.16 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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: http://hdl.handle.net/10281/142448
Citazioni
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 6
Social impact