Temporal Equilibrium Logic with past operators

摘要

In this paper, we study the introduction of modal past temporal operators in Temporal Equilibrium Logic (TEL), an hybrid formalism that mixes linear-time modalities and logic programs interpreted under stable models and their characterisation in terms of Equilibrium Logic. We show that Kamp's translation can also be used to translate the new extension of TEL with past operators into Quantified Equilibrium Logic. Additionally, we provide a method for removing past operators that consists in replacing past-time subformulas by fresh auxiliary atoms, obtaining an equivalent formula, modulo the original alphabet.