为含条件谓词和算术的逻辑程序提供无需预处理的新语义
SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
- 基于SM算子构建新语义，避免传统方法的预处理步骤
- 证明新旧两种语义在逻辑上完全等价
- 适合需要高效推理的知识表示研究者
现代答案集编程求解器（如CLINGO）支持增强语言构造，提升逻辑程序的表达力与简洁性。条件谓词作为其中一种构造，在规则体中形成类似嵌套蕴含的子公式，使规则形式更接近一阶逻辑的非限制语法。这类特性使其成为知识表示的有效工具。本文提出一种基于SM算子的语义框架，适用于含条件谓词与算术运算的逻辑程序。该语义无需先验地进行展开（grounding），不同于现有依赖无穷命题逻辑转换的语义方法。本文的核心成果是建立新语义与已有语义之间的精确对应关系。
原文摘要 · Abstract (English)
Modern answer set programming solvers such as CLINGO support advanced language constructs that improve the expressivity and conciseness of logic programs. Conditional literals are one such construct. They form "subformulas" that behave as nested implications within the bodies of logic rules. Their inclusion brings the form of rules closer to the less restrictive syntax of first-order logic. These qualities make conditional literals useful tools for knowledge representation. In this paper, we propose a semantics for logic programs with conditional literals and arithmetic based on the SM operator. These semantics do not require grounding, unlike the established semantics for such programs that relies on a translation to infinitary propositional logic. The main result of this paper establishes the precise correspondence between the proposed and existing semantics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。