Herbrand Methods in Sequent Calculi: Unification in LL.
Serenella Cerrito · 1992
We propose a reformulation of quantifiers rules in sequent calculi which allows to replace blind existential instantiation with unification, thereby reducing nondeterminism and complexity in proof-search. Our method, based on some ideas underlying the proof of Herbrand theorem for classical logic, may be applied to any "reasonable" non-classical sequent calculus, but here we focus on sequent calculus for linear logic, in view of an application to linear logic programming. We prove that the new linear proof-system which we propose, the so called system LLH, is equivalent to standard linear sequent calculus LL. 1 Introduction A result in classical logic which has been widely exploited in logic programming is Herbrand theorem. Several versions of this result are present in the literature; we recall here one of them (see [13]). Herbrand Theorem Let F be a prenex formula of the form 9w8x9y8zA[w; x; y; z] with A quantifier-free. F is provable in predicate calculus if and only if a disjun...