t 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 näive 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 which prevents the generation of infinite branches by storing and analyzing some information regarding the branch under development. In this paper we propose a new technique based on evaluation functions. An evaluation function is a lightweight computational mechanism which, analyzing only the current goal of the proof-search, allows one to drive the application of rules so 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 counter-model 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.

An evaluation-driven decision procedure for G3i

FERRARI, MAURO;
2015

Abstract

t 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 näive 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 which prevents the generation of infinite branches by storing and analyzing some information regarding the branch under development. In this paper we propose a new technique based on evaluation functions. An evaluation function is a lightweight computational mechanism which, analyzing only the current goal of the proof-search, allows one to drive the application of rules so 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 counter-model 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.
http://www.acm.org/tocl/
Intuitionistic propositional logic; Proof-search procedures; Sequent calculi; Computer Science (all); Theoretical Computer Science; Computational Mathematics; Logic
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11383/2024187
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 6
social impact