SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic

TL;DR

This work provides a grounding-free semantics for logic programs that mix conditional literals and arithmetic by using the $SM$ operator on a many-sorted FO translation ($ au^*$). It unifies prior approaches by showing that $SM$-based semantics for these features coincide with the established infinitary propositional semantics underlying gringo/Clingo, thereby enabling modular verification and reasoning without grounding. The introduction of the $p$-answer set notion separates intensional from extensional predicates, supporting modular reasoning and refactoring of encodings. Overall, the paper delivers a principled, grounding-free framework that aligns SM-based characterizations with clingo's semantics and suggests directions for simplification and automated verification tooling.

Abstract

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.