Accession Number : ADA326173
Title : Temporal Logic Programming is Complete and Expressive,
Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Baudinet, Marianne
PDF Url : ADA326173
Report Date : OCT 1988
Pagination or Media Count : 16
Abstract : This paper addresses semantic and expressiveness issues for temporal logic programming and in particular for the TEMPLOG language proposed by Abadi and Manna. Two equivalent formulations of TEMPLOG's declarative semantics are given: in terms of a minimal Herbrand model and in terms of a least fixpoint. By relating these semantics to TEMPLOG's operational semantics, we prove the completeness of the resolution proof system underlying TEMPLOG's execution mechanism. To study TEMPLOG's expressiveness, we consider its propositional version. We show how propositional TEMPLOG programs can be translated into a temporal fixpoint calculus and prove that they can express essentially all regular properties of sequences.
Descriptors : *COMPUTER LOGIC, *PROGRAMMING LANGUAGES, *SEMANTICS, FORMULATIONS, COMPUTER PROGRAMMING, SEQUENCES.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE