Report Number: CS-TR-88-1203
Institution: Stanford University, Department of Computer Science
Title: On the Semantics of Temporal Logic Prograrnrning
Author: Baudinet, Marianne
Date: June 1988
Abstract: Recently, several researchers have suggested directly exploiting in a programming language temporal logic's ability to describe changing worlds. The resulting languages are quite diverse. They are based on different subsets of temporal logic and use a variety of execution mechanisms. So far, little attention has been paid to the formal semantics of these languages. In this paper, we study the semantics of an instance of temporal logic programming, namely, the TEMPLOG language defined by Abadi and Manna. We first give declarative semantics for TEMPLOG, in model-theoretic and in fixpoint terms. Then, we study its operational semantics and prove soundness and completeness theorems for the temporal-resolution proof method underlying its execution mechanism.
http://i.stanford.edu/pub/cstr/reports/cs/tr/88/1203/CS-TR-88-1203.pdf