用元编程框架统一实现多种时序逻辑，让快速实验新逻辑成为可能。
Meta-Programming for Linear-time Temporal Answer Set Programming
- 通过扩展clingo语法，用声明式方式统一定义不同时间逻辑
- 解决嵌套模态在求解中被错误简化的问题，保证语义正确性
- 适合逻辑研究者快速验证新时序系统设计
时序答案集编程（ASP）的发展催生了非单调线性时间（TEL）、动态（DEL）和度量（MEL）时序平衡逻辑。然而，高度优化的ASP系统固有的刚性常阻碍对替代逻辑设计的快速探索与实现。本文提出一种灵活的元编程框架，通过统一的声明式机制实现多种时序逻辑的语义。该方法在clingo理论语法中引入形式类型规范和嵌套能力，并设计转换流水线，在接地过程中保护嵌套模态免受基于稳定模型的简化。我们通过实现TEL、MEL和DEL的元编码展示了框架的可扩展性。特别地，我们详述了TEL的完整描述，并阐明了管理MEL区间约束与DEL Fischer-Ladner闭包的关键特性。最后，我们推出了metasp系统，封装了这一工作流程。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。