Abstract
Recent development of logic programming languages based on linear logic suggests a successful direction to extend logic programming to be more expressive and more efficient. The treatment of formulasas- resources gives us not only powerful expressiveness, but also efficient access to a large set of data. However, in linear logic, whole resources are kept in one context, and there is no straight way to represent complex data structures as resources. For example, in order to represent an ordered list and time-dependent data, we need to put additional indices for each resource formula. This paper describes a logic programming language, called TLLP, based on intuitionistic temporal linear logic. This logic, an extension of linear logic with some features from temporal logics, allows the use of the modal operators ‘◯’(next-time) and ‘□’(always) in addition to the operators used in intuitionistic linear logic. The intuitive meaning of modal operators is as follows: ◯B means that B can be used exactly once at the next moment in time; □B means that B can be used exactly once any time; !B means that B can be used arbitrarily many times (including 0 times) at any time. We first give a proof theoretic formulation of the logic of the TLLP language. We then present a series of resource management systems designed to implement not only interpreters but also compilers based on an extension of the standard WAM model.
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
Jean-Marc Andreoli and Remo Pareschi. Linear objects: Logical processes with built-in inheritance. New Generation Computing, 9:445–473, 1991.
Mutsunori Banbara and Naoyuki Tamura. Compiling Resources in a Linear Logic Programming Language. In Konstantinos Sagonas, editor, Proceedings of the JICSLP’98 Post Conference Workshop 7 on Implementation Technologies for Programming Languages based on Logic, pages 32–45, June 1998.
Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. In R. Dyckho., H. Herre, and P. Schroeder-Heister, editors, Proceedings of the Fifth International Workshop on Extensions of Logic Programming-ELP’96, pages 67–81, Leipzig, Germany, 28–30 March 1996. Springer-Verlag LNAI 1050.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
James Harland and David Pym. A uniform proof-theoretic investigation of linear logic programming. Journal of Logic and Computation, 4(2):175–207, April 1994.
Takaharu Hirai. An Application of Temporal Linear Logic to Timed Petri Nets. In Proceedings of the Petri Nets’99 Workshop on Applications of Petri Nets to Intelligent System Development, pages 2–13, June 1999.
Joshua S. Hodas. Logic Programming in Intuitionistic Linear Logic: Theory, Design and Implementation. PhD thesis, University of Pennsylvania, Department of Computer and Information Science, 1994.
Joshua S. Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327–365, 1994. Extended abstract in the Proceedings of the Sixth Annual Symposium on Logic in Computer Science, Amsterdam, July 15–18, 1991.
Joshua S. Hodas, Kevin Watkins, Naoyuki Tamura, and Kyoung-Sun Kang. Efficient Implementation of a Linear Logic Programming Language. In Joxan Jaffar, editor, Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming, pages 145–159. The MIT Press, June 1998.
Kyoung-Sun Kang, Mutsunori Banbara, and Naoyuki Tamura. Efficient resource management model for linear logic programming languages. Computer Software, 18(0):138–154, 2001. (in Japanese).
Max I. Kanovich and Takayasu Ito. Temporal linear logic specifications for concurrent processes (extended abstract). In Proceedings of 12th Annual IEEE Symposium on Logic in Computer Science (LICS’97), pages 48–57, 1997.
Naoki Kobayashi and Akinori Yonezawa. ACL-A concurrent linear logic programming paradigm. In D. Miller, editor, Proceedings of the 1993 International Logic Programming Symposium, pages 279–294, Vancouver, Canada, October 1993. MIT Press.
Dale Miller. A multiple-conclusion specification logic. Theoretical Computer Science, 165(1):201–232, 1996.
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.
Naoyuki Tamura and Yukio Kaneda. Extension of WAM for a linear logic programming language. In T. Ida, A. Ohori, and M. Takeichi, editors, Second Fuji International Workshop on Functional and Logic Programming, pages 33–50.World Scientific, Nov. 1996.
Makoto Tanabe. Timed petri nets and temporal linear logic. In Lecture Notes in Computer Science 1248: Proceedings of Application and Theory of Petri Nets, pages 156–174, June 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banbara, M., Kyoung-Sun, K., Hirai, T., Tamura, N. (2001). Logic Programming in a Fragment of Intuitionistic Temporal Linear Logic. In: Codognet, P. (eds) Logic Programming. ICLP 2001. Lecture Notes in Computer Science, vol 2237. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45635-X_29
Download citation
DOI: https://doi.org/10.1007/3-540-45635-X_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42935-7
Online ISBN: 978-3-540-45635-3
eBook Packages: Springer Book Archive