Towards Dynamic Answer Set Programming over Finite Traces

Abstract

Our ultimate goal is to conceive an extension of Answer Set Programming with language constructs from dynamic (and temporal) logic to provide an expressive computational framework for modeling dynamic applications. To address this in a semantically well founded way, we generalize the definition of Dynamic Equilibrium Logic to accommodate finite linear time and extend it with a converse operator in order to capture past temporal operators. This results in a general logical framework integrating existing dynamic and temporal logics of Here-and-There over both finite and infinite time. In the context of finite time, we then develop a translation of dynamic formulas into propositional ones that can in turn be translated into logic programs.