arXiv:2507.13958cs.AIcs.LO2025-07

为逻辑编程引入带约束的精细时序推理,解决动态系统建模难题。

Towards Constraint Temporal Answer Set Programming

  • 融合时序逻辑与约束逻辑,实现高精度非单调时序推理。
  • 首次在ASP中构建支持数值约束的非单调时序框架。
  • 适合需精确建模时间与约束关系的研究者使用。

基于逻辑的推理方法(如答案集编程,ASP)在处理具有细粒度时间与数值分辨率的动态系统时面临重大挑战。为此,本文提出并深入研究了一种新颖的时序约束扩展逻辑——基于“此处与那里”逻辑及其非单调均衡扩展,据我们所知,这是首个专为ASP设计的非单调时序约束推理方法。该表达力强的系统通过两种基础ASP扩展的协同结合实现:线性时序的“此处与那里”逻辑,提供稳健的非单调时序推理能力;以及带约束的“此处与那里”逻辑,支持直接集成与操作数值约束等。本工作为在ASP范式下处理高分辨率复杂动态系统建立了基础逻辑框架。

原文摘要 · Abstract (English)

Reasoning about dynamic systems with a fine-grained temporal and numeric resolution presents significant challenges for logic-based approaches like Answer Set Programming (ASP). To address this, we introduce and elaborate upon a novel temporal and constraint-based extension of the logic of Here-and-There and its nonmonotonic equilibrium extension, representing, to the best of our knowledge, the first approach to nonmonotonic temporal reasoning with constraints specifically tailored for ASP. This expressive system is achieved by a synergistic combination of two foundational ASP extensions: the linear-time logic of Here-and-There, providing robust nonmonotonic temporal reasoning capabilities, and the logic of Here-and-There with constraints, enabling the direct integration and manipulation of numeric constraints, among others. This work establishes the foundational logical framework for tackling complex dynamic systems with high resolution within the ASP paradigm.

逻辑编程时序推理约束求解

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。