Search papers, labs, and topics across Lattice.
This paper introduces a meta-programming framework for Answer Set Programming (ASP) that enables the flexible implementation of various temporal logics like TEL, MEL, and DEL. The framework extends ASP meta-programming with type specifications and nesting capabilities within clingo's theory grammar, and uses a transformation pipeline to prevent premature simplification of nested modalities. The authors demonstrate the framework's extensibility by providing meta-encodings for TEL, MEL, and DEL, and encapsulate the workflow in a tool called metasp.
Unlock rapid prototyping of temporal reasoning systems: this meta-programming framework lets you implement and experiment with different temporal logics within Answer Set Programming without wrestling with the rigidity of optimized ASP systems.
The development of temporal extensions of Answer Set Programming (ASP) has led to the emergence of non-monotonic linear-time (TEL), dynamic (DEL), and metric (MEL) temporal equilibrium logics. However, the inherent rigidity of highly optimized ASP systems often hinders the rapid exploration and implementation of alternative logical designs. In this work, we propose a flexible meta-programming framework that operationalizes the semantics of varied temporal logics through a unified, declarative framework. Our approach extends standard ASP meta-programming by augmenting clingo's theory grammar with formal type specifications and nesting capabilities. To ensure semantic correctness, we introduce a transformation pipeline that protects nested modalities from stable-model-based simplifications during grounding. We demonstrate the extensibility of our framework by implementing meta-encodings for TEL, MEL, and DEL. We provide a comprehensive account of TEL and highlight the key features for managing the interval constraints of MEL and the Fischer-Ladner closure in DEL. Finally, we introduce the metasp system, a versatile tool that encapsulates this workflow.