Journal of Logic, Language and Information 2 (1):59-83 (1993)
|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||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Michael Kohlhase (1999). Higher-Order Multi-Valued Resolution. Journal of Applied Non-Classical Logics 9 (4):455-477.
Sara Negri (2002). Varieties of Linear Calculi. Journal of Philosophical Logic 31 (6):569-590.
Matthias Baaz & Rosalie Iemhoff (2006). Gentzen Calculi for the Existence Predicate. Studia Logica 82 (1):7 - 23.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Marcelo Finger & Dov M. Gabbay (1992). Adding a Temporal Dimension to a Logic System. Journal of Logic, Language and Information 1 (3):203-233.
Peter Schroeder-Heister (2002). Resolution and the Origins of Structural Reasoning: Early Proof-Theoretic Ideas of Hertz and Gentzen. Bulletin of Symbolic Logic 8 (2):246-265.
Christoph Benzmüller (2002). Comparing Approaches to Resolution Based Higher-Order Theorem Proving. Synthese 133 (1-2):203 - 235.
Added to index2009-01-28
Total downloads15 ( #85,899 of 722,750 )
Recent downloads (6 months)1 ( #60,247 of 722,750 )
How can I increase my downloads?