Time-extraction for temporal logic -- logic programming and local process time (Q1333399)

Models of modal logics are usually sets of ``possible worlds'' related by some ``accessibility'' relations. In the particular case of temporal logic the different worlds represent different time instants and are ordinated according to the flow of time. Thus an interpretation in this case can be seen as an infinite sequence of standard FOL interpretations. The paper introduces the notion of ``time-extraction'' for these temporal interpretations: Given a sequence of worlds \(S\) and a formula \(F\), a subsequence \(S'\) is extracted from \(S\) by considering only those worlds in which \(F\) is true. Then it is shown that, for certain formulas, the truth in the sequence \(S\) can be derived from the truth in the extracted sequence \(S'\). This result is applied to provide a modular semantics for a temporal logic programming language.