Strong Equivalence of Non-Monotonic Temporal Theories
Pedro Cabalar, Martín Diéguez · 2014
In this paper we solve the following open problem: we prove that equivalence in the logic of Temporal Here-and-There (THT) is not only a sufficient, but also a necessary condition for strong equivalence of two Temporal Equilibrium Logic (TEL) theories. This result has allowed constructing a tool, ABSTEM, that can be used to check different types of equiv-alence between two arbitrary temporal theories. More impor-tantly, when the theories are not THT-equivalent, the system provides a context theory that makes them behave differently, together with a Büchi automaton showing the temporal stable models that arise from that difference.