Executing Metric Temporal Logic

this paper, we present a solution to the problem of supporting derivability in metric temporal logic based on a set-theoretic translation method. In order to execute metric temporal logic, we first transforms it into a polymodal logic with infinitely many modalities, and then reduces derivability in such a polymodal logic to derivability in a suitable first-order set theory. As noticed in [7], compared with the direct approach of finding a proof algorithm for a specific class of modal logics, the translation methods have the advantage of being independent of the particular modal logic under consideration: a single theorem prover may be used for any translatable modal logic. In [7, 5, 6], a set-theoretic translation method (2-as-P ow translation, from now on) for (poly)modal logics has been proposed, whose basic idea is to map modal formulae into set-theoretic terms. Such a method can be applied to all normal, finitely axiomatizable modal logics, regardless of their frame completeness and the first-order axiomatizability of their semantics. Moreover, the 2-as-Pow translation works also when the modal logic is specified by Hilbert axioms only. Furthermore, it can be easily generalized to polymodal logics with finitely many modalities. In this paper, we consider the problem of applying the 2-as-Pow translation to metric temporal logic (MTL for short). MTL extends propositional logic with a parametrized operator r ff of temporal realization [10, 11, 12, 13]. Such an operator allows one to constrain the truth value of a proposition at time instants different from the current one, which is left implicit. If we interpret the parameter ff as a temporal displacement with respect to the current time instant, P ff q is true at the time instant i if and only if q is true at the tim..