Abstract
In this work we consider the additive and multiplicative linear logic (AMLL) with an automated deduction point of view. Considering this recent logical framework and its possible extensions or applications to logic programming, programming with proofs or parallelism and concurrency, we propose a new algorithm that constructs a proof for a given sequent in AMLL and its termination, correctness and completeness proofs. It can be viewed as a direct (or constructive) proof of the decidability of AMLL and as a first step to consider linear logic as a basis for an extended programming logic. The restriction (and adaptation) of this result to multiplicative linear logic (MLL) gives an adequate algorithm for automatic proof net construction.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky. Computational interpretations of linear logic. technical report, Department of Computing, Imperial College, London SW7 2Bz, England, 1991.
J.M. Andreoli and R. Pareschi. Linear objects: Logical processes with built in inheritance. In 7th international conference of logic programming, pages 495–510, Jerusalem, June 1990. MIT Press.
G. Bellin. Proof nets for multiplicative and additive linear logic. Technical Report ECS-LFCS 91-161, Department of Computer Science, Edinburgh University, May 1991.
S. Cerrito. A linear semantics for allowed logic programs. In 5th IEEE Symposium on Logic in Computer Science, pages 219–227, Philadelphia, June 1990.
V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181–203, 1989.
D. Galmiche. The power of constructive framework for program synthesis. In COLOG 88 — International Conference on Computer Logic, Tallinn, Estonia, USSR, December 1988.
D. Galmiche. Constructive system for automatic program synthesis. Theoretical Computer Science, 71(2):227–239, 1990.
J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1): 1–102,1987.
J.-Y. Girard. Towards a geometry of interaction. In J.-W. Gray and A. Scedrov, editors, AMS Conference on categories in computer science and logic, pages 69–108, Boulder-Colorado, June 1987.
J. S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In 6th IEEE symposium Logic in Computer Science, pages 32–42, Amsterdam, July 1991.
J. Vauzeilles M. Masseron, C. Tollu. Generating plans in linear logic. In Foundations of Software Technology and Theoretical Computer Science, LNCS 472, pages 63–65, Bangalore, India, December 1990.
A. Scedrov P. Lincoln, J. Mitchell and N. Shankar. Decision problems for propositional linear logic. In 31st annual IEEE Symp. on Foundations of Computer Science, St-Louis, Missouri, October 1990.
U. Solitro. A typed calculus based on a fragment of linear logic. Theoretical Computer Science, 68:333–342,1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Galmiche, D., Perrier, G. (1992). Automated deduction in additive and multiplicative linear logic. In: Nerode, A., Taitslin, M. (eds) Logical Foundations of Computer Science — Tver '92. LFCS 1992. Lecture Notes in Computer Science, vol 620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023870
Download citation
DOI: https://doi.org/10.1007/BFb0023870
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55707-4
Online ISBN: 978-3-540-47276-6
eBook Packages: Springer Book Archive