Journal of Logic, Language and Information 2 (1):59-83 (1993)
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|
|Categories||categorize this paper)|
References found in this work BETA
Uniform Proofs as a Foundation for Logic Programming.Dale Miller, Gopalan Nadathur, Frank Pfenning & Andre Scedrov - 1991 - Annals of Pure and Applied Logic 51 (1-2):125-157.
The Uniform Proof-Theoretic Foundation of Linear Logic Programming.J. A. Harland & D. J. Pym - 1991 - LFCS, Department of Computer Science, University of Edinburgh.
Citations of this work BETA
No citations found.
Similar books and articles
Higher-Order Multi-Valued Resolution.Michael Kohlhase - 1999 - Journal of Applied Non-Classical Logics 9 (4):455-477.
Adding a Temporal Dimension to a Logic System.Marcelo Finger & Dov M. Gabbay - 1992 - Journal of Logic, Language and Information 1 (3):203-233.
Resolution and the Origins of Structural Reasoning: Early Proof-Theoretic Ideas of Hertz and Gentzen.Peter Schroeder-Heister - 2002 - Bulletin of Symbolic Logic 8 (2):246-265.
Comparing Approaches to Resolution Based Higher-Order Theorem Proving.Christoph Benzmüller - 2002 - Synthese 133 (1-2):203 - 235.
Added to index2009-01-28
Total downloads26 ( #196,918 of 2,171,932 )
Recent downloads (6 months)1 ( #326,558 of 2,171,932 )
How can I increase my downloads?