arXiv:2511.19565cs.LOcs.AI2025-11被引 1

扩展演绎系统以证明带计数的逻辑程序强等价性

Deductive Systems for Logic Programs with Counting

  • 构建支持计数聚合的演绎系统
  • 实现含计数规则的程序强等价判定
  • 适用于答案集编程中的形式化验证

在答案集编程中,若两个规则组在任何上下文中含义相同,则认为它们是强等价的。有时可通过在一个合适的演绎系统中相互推导出对方的规则来证明这种强等价性。本文展示了如何将这一方法扩展到包含计数聚合的逻辑程序。

原文摘要 · Abstract (English)

In answer set programming, two groups of rules are considered strongly equivalent if they have the same meaning in any context. Strong equivalence of two programs can be sometimes established by deriving rules of each program from rules of the other in an appropriate deductive system. This paper shows how to extend this method of proving strong equivalence to programs containing the counting aggregate.

逻辑编程强等价计数聚合

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