Resolution calculus for the first order linear logic
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 | ||||||||||
| Options |
|
|||||||||
| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,631 |
| External links |
|
| Through your library | Configure |
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.
Monthly downloads |
Added to index2009-01-28Total downloads15 ( #78,526 of 548,973 )Recent downloads (6 months)1 ( #63,511 of 548,973 )How can I increase my downloads? |

