Paper Info
Title
Resolution calculus for the first order linear logic.
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.
Year
DOI
Venue
1993
10.1007/BF01051768
Journal of Logic, Language and Information
Keywords
Field
DocType
resolution,linear logic,automated deduction
Discrete mathematics,Geometry of interaction,Zeroth-order logic,Bunched logic,Resolution (logic),Linear logic,Predicate logic,Mathematics,Higher-order logic,Calculus,Intermediate logic
Journal
Volume
Issue
Citations 
2
1
13
PageRank 
References 
Authors
1.21
6
1
Name
Order
Citations
PageRank
Grigori Mints123572.76