A simple proof of the completeness of ternporal logic programming
Marianne Baudinet · 1992
Abstract We address semantic and completeness issues for temporal logic programming, and in particular for the language Templog proposed by Abadi and Manna. We show that the semantic and completeness results for classical logic programming can be extended to TEMP LOG. We thus provide two equivalent formulations of Templog’s declarative semantics, in terms of a minimal model and in terms of a least fixpoint, and we prove the completeness of the temporal resolution proof system that is the basis of Templog’s execution mechanism.