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