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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Andreoli, J. and Paresci, R., 1990, “Linear Objects: Logical processes with built-in inheritance,”New Generation Computing, Special issue, Selected Papers of ICLP'90.
Girard, J.-Y., 1987, “Linear Logic,”Theoretical Computer Science 50:1, 1–101.
Harland, J. and Pym, D., 1991, “The Uniform Proof-Theoretic Foundation of Linear Logic Programming,”Proceedings of the 1991 International Symposium on Logic Programming, MIT Press, 304–320.
Hodas, J. and Miller, D., 1991, “Logic Programming in a fragment of Intuitionistic Linear Logic,”Proceedings of sixth Annual IEEE Symp. on Logic in Computer Science, IEEE Computer Society Press.
Kleene, S. C., 1974,Introduction to Metamathematics, North-Holland.
Maslov, S., 1968, “Inverse method of establishing deducibility for logical calculi,”Proc. Steklov inst. of Math. 98.
Maslov, S., 1971, “Deduction-search tactics based on the unification of order of terms in a favourable set,”Seminars in Mathematics 16, Plenum Press, New York.
Maslov, S., 1969, “The connection between tactics of inverse method and the resolution method,” A. O. Slisenko, ed., Zapiski Nauchnykh Seminarov LOMI. v. 16, English translation in: “J. Siekmann, G. Wrightson, eds. Automated Reasoning,” Springer-Verlag, Berlin, 1983, v2., 264–27.
Maslov, S. and Mints, G., 1983, “Proof Search Theory and the Inverse Method (Russian),” Supplement to the Russian translation of the book by Chang and Lee. Moscow. Nauka, 310–340.
Miller, D., Nadatur, G., Pfennig, F. and Scedrov, A., 1991, “Proofs as a Foundation for the Logic Programming,”Annals of Pure and Applied Logic 51, 125–127.
Mints, G., 1981, “Resolution Calculi for Non-classical Logics” (Russian),9-th Soviet Symposium in Cybernetics, v. 2, 34–36.
Mints, G., 1985, “Resolution Calculi for Non-classical Logics” (Russian).Semiotika i Informatika 25, 120–135.
Mints, G., 1990, “Gentzen-type Systems and Resolution Rule. Part I. Propositional Logic,”Lecture Notes in Computer Sci. 417, 198–231.
Mints, G., “Gentzen-type Systems and Resolution Rule. Part II,”Logic Colloquium '90, (to be published).
Tammet, T., “Proof Search in Linear Logic,” (Submitted).
Zamov, N., 1987, “The Resolution Method without Skolemization,”Soviet Math. Dokl. 35, N2, 399–401.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Mints, G. Resolution calculus for the first order linear logic. J Logic Lang Inf 2, 59–83 (1993). https://doi.org/10.1007/BF01051768
Received:
Revised:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF01051768