Resolution calculus for the first order linear logic (Q1314284): Difference between revisions

This paper presents a formulation and completeness proof of the resolution-type calculi for the first order fragment of Girard's linear logic by a general method which provides the general scheme of transforming a cut-free Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. Ideas of the author and Zamov are used to avoid Skolemization. Completeness of strategies is first established for the Gentzen-type system, and then transferred to resolution. The propositional resolution sustem was implemented by \textit{T. Tammet} [``Proof search strategies for linear logic'', J. Autom. Reasoning (to appear)]. This computer program was successful due to several additional strategies derived from the connection with Gentzen-type systems.