Resolution calculus for the first order linear logic |
| |
Authors: | Grigori Mints |
| |
Affiliation: | (1) Department of Philosophy, Stanford University, 94305 Stanford, CA |
| |
Abstract: | 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 cutfree 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 skolomization. Completeness of strategies is first established for the Gentzen-type system, and then transferred to resolution. The propositional resolution system was implemented by T. Tammet. |
| |
Keywords: | resolution linear logic automated deduction |
本文献已被 SpringerLink 等数据库收录! |
|