Temporal Logic Programming is Complete and Expressive,

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1988
Accession Number
ADA326173

Entities

People

  • Marianne Baudinet

Organizations

  • Stanford University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Alphabets
  • Artificial Intelligence
  • Automata
  • Availability
  • Calculus
  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Language
  • Programming Languages
  • Semantics
  • Sequences
  • Symbols
  • Universities

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computational Linguistics
  • Computer Engineering