Abstract
Linear logic provides a logical framework to express fundamental computational concepts in a declarative style. As a consequence, it has been used as a sound foundation for the design of expressive programming and specification languages. Unfortunately, linearity is as convenient for specifying as difficult to implement. In particular, the successful implementation of linear logic languages and provers involving context splitting strongly depends on the efficiency of the method computing a suitable split. A number of solutions have been proposed, referred to as lazy splitting or resource management systems. In this paper, we present a new resource management system for the Lolli linear logic language. We show that the choice of the structure employed to represent the contexts has a strong influence on the overall performance of the resource management system. We also estimate the performance of previous proposals, and compare them to our new system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J.M. Andreoli and R. Pareschi. Linear Objects: Logical Processes with Built-in Inheritance. New Generation Computing, 9(3–4):445–473, 1991.
I. Cervesato, J. Hodas, and F. Pfenning. Efficient Resource Management for Linear Logic Proof Search. Proceedings of the 1996 International Workshop on Extensions of Logic Programming, 1996.
J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50, pp. 1–102. 1987.
J.S. Hodas. Logic. Programming in Intuitionistic Linear Logic: Theory, Design and Implementation. PhD Thesis. University of Pennsylvania, Department of Computer and Information Science, 1994.
J.S. Hodas and D. Miller. Logic Programming in a Fragment of Intuitionistic Linear Logic. Information and Computation, 110(2), pp. 327–365, 1994.
N. Kobayashi and A. Yonezawa. ACL — a Concurrent Linear Logic Programming Paradigm. In International Logic Programming Symposium, pp. 279–294, 1993.
P. López. Implementación de un Lenguaje de Programación basado en Lógica Lineal. Master’s Thesis supervised by E. Pimentel. Computer Science Department. University of Malaga. 1996.
P. López and E. Pimentel. A Lazy Splitting System for Forum. In M. Falaschi, M. Navarro, and A. Policriti, editors, Proceedings of the Joint Conference on Declarative Programming — APPIA-GULP-PRODE’97, pp. 247–258, Grado, Italy, 1997.
P. López and E. Pimentel. Resource Managament for Linear Logic Proof Search. Manuscript, 1999.
D. Miller. A Multiple-Conclusion Meta-Logic. S. Abramsky, editor, Proceedings of the 1994 Symposium on Logic in Computer Science, pp. 272–281, 1994.
D. Miller. Forum: A Multiple-Conclusion Specification Logic. Theoretical Computer Science, 165(1), pp.201–232, 1996.
C. Urban. Forum and its Implementation. MPhil Thesis. Department of Computer Science, University of St. Andrews, 1996.
M. Winikoff and J. Harland. Implementing the Linear Logic Programming Language Lygon. In J. Lloyd, editor, Proceedings of the 1995 International Logic Programming Symposium, pp. 66–80, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
López, P., Pimentel, E. (1999). Resource Management in Linear Logic Proof Search Revisited. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds) Logic for Programming and Automated Reasoning. LPAR 1999. Lecture Notes in Computer Science(), vol 1705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48242-3_19
Download citation
DOI: https://doi.org/10.1007/3-540-48242-3_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66492-5
Online ISBN: 978-3-540-48242-0
eBook Packages: Springer Book Archive