Abstract
In this paper, we consider the multiplicative fragment of linear logic (MLL) from an automated deduction point of view. Before to use this new logic to make logic programming or to program with proofs, a better comprehension of the proof construction process in this framework is necessary. We propose a new algorithm to construct automatically a proof net for a given sequent in MLL and its proofs of termination, correctness and completeness. It can be seen as an implementation oriented way to consider automated deduction in linear logic.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
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. Logic programming with sequent systems: A linear logic approach. In Int. Workshop on Extensions of Logic Programming, LNCS 475, pages 1–30, Tübingen, Germany, December 1989.
P. Andrews. Theorem proving via general mating. Journal of ACM, 28(2):193–214, 1981.
G. Bellin. Proof nets for multiplicative and additive linear logic. Technical Report ECS-LFCS 91-161, Department of Computer Science, Edinburgh University, May 1991.
W. Bibel. On matrices with connections. Journal of ACM, 28(4):633–645, 1981.
V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181–203, 1989.
D. Galmiche. Constructive system for automatic program synthesis. Theoretical Computer Science, 71(2):227–239, 1990.
D. Galmiche and G. Perrier. Automated deduction in additive and multiplicative linear logic. In Logic at Tver '92, Logical Foundations of Computer Science Symposium, Tver, Russia, July 1992.
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.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University Press, 1989.
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.
P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for prepositional linear logic. In 31st annual IEEE Symp. on Foundations of Computer Science, St-Louis, Missouri, October 1990.
M. Masseron, C. Tollu, and J. Vauzeilles. Generating plans in linear logic. In Foundations of Software Technology and Theoretical Computer Science, LNCS 472, pages 63–75, Bangalore, India, December 1990.
U. Solitro. A typed calculus based on a fragment of linear logic. Theoretical Computer Science, 68:333–342, 1989.
A.-S. Troelstra and D. Van Dalen. Constructivism in Mathematics, an Introduction. North-Holland, Amsterdam, 1988.
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). A procedure for automatic proof nets construction. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1992. Lecture Notes in Computer Science, vol 624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013047
Download citation
DOI: https://doi.org/10.1007/BFb0013047
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55727-2
Online ISBN: 978-3-540-47279-7
eBook Packages: Springer Book Archive