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-01-01
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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
