Adding a temporal dimension to a logic system (Q1314287)

A methodology is introduced in which an arbitrary logic system \(L\) can be embedded into a temporal logic system \(T\), which enriches \(L\) with temporal features. The method used is not confined to temporalisation only, but is a methodology of combining any two logics by substituting one in another. In this paper the underlining system \(L\) characterizes the local behaviour of a database distributed in time, whereas the upper level temporal logic \(T\) describes the evolution of the database. The resulting logic system \(T(L)\) enables us to reason about the ``temporal network'' as a whole. The idea of temporalising a logic system \(L\) in terms of a (since, until) temporal system \(T\) is formalized and the soundness and completeness of \(T(L)\) over linear time is proved. Moreover, \(T(L)\) preserves the decidability of \(L\) over linear time, and the complexity of the decision procedure is estimated. It is shown that \(T(L)\) is a conservative extension of \(L\) and that it has the separation property (which enables us to follow the changes of the database states in time). As a special interesting application, temporalisation of first-order logic \(L\) is discussed. In a general case, when the upper system is a propositional modal logic system \(M\), a modalised system \(M(L)\) can be derived. If the logic \(L\) has a possible world semantics, each possible world can be substituted by a model of \(L\), so as to construct a model for the system \(M(L)\).