Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Logic Programming in a Fragment of Intuitionistic Temporal Linear Logic
| Book Series | Lecture Notes in Computer Science |
| Publisher | Springer Berlin / Heidelberg |
| ISSN | 0302-9743 (Print) 1611-3349 (Online) |
| Volume | Volume 2237/2001 |
| Book | Logic Programming |
| DOI | 10.1007/3-540-45635-X |
| Copyright | 2001 |
| ISBN | 978-3-540-42935-7 |
| DOI | 10.1007/3-540-45635-X_29 |
| Pages | 315-330 |
| Subject Collection | Computer Science |
| SpringerLink Date | Monday, January 01, 2001 |
| |
|
Logic Programming in a Fragment of Intuitionistic Temporal Linear Logic
Mutsunori Banbara6 , Kyoung-Sun Kang 7 , Hirai Takaharu 5 and Naoyuki Tamura8 
| (5) |
Graduate School of Science and Technology, Kobe University, 1-1 Rokkodai, Nada, 657-8501 Kobe, Japan |
| (6) |
Department of Mathematics, Nara National College of Technology, 22 Yata, Yamatokoriyama, 639-1080, Japan |
| (7) |
Department of Computer Engineering, Pusan University of Foreign Studies, 55-1, Uam-dong, Nam-gu, 608-738 Pusan, Korea |
| (8) |
Department of Computer and Systems Engineering, Kobe University, 1-1 Rokkodai, Nada, 657-8501 Kobe, Japan |
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.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|