On the Semantics of Gringo
Input languages of answer set solvers are based on the mathematically simple concept of a stable model. But many useful constructs available in these languages, including local variables, conditional literals, and aggregates, cannot be easily explained in terms of stable models in the sense of the original definition of this concept and its straightforward generalizations. Manuals written by designers of answer set solvers usually explain such constructs using examples and informal comments that appeal to the user's intuition, without references to any precise semantics. We propose to approach the problem of defining the semantics of gringo programs by translating them into the language of infinitary propositional formulas. This semantics allows us to study equivalent transformations of gringo programs using natural deduction in infinitary propositional logic.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
Answer Set Programming Modulo Theories (ASPMT) is an approach to combining answer set programming and satisfiability modulo theories based on the functional stable model semantics. It is shown that the tight fragment of …
Verifying Tight Logic Programs with anthem and Vampire
This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a sub…
LEMMAOn the Foundations of Grounding in Answer Set Programming
We provide a comprehensive elaboration of the theoretical foundations of variable instantiation, or grounding, in Answer Set Programming (ASP). Building on the semantics of ASP's modeling language, we introduce a formal …
Clingcon: The Next Generation
We present the third generation of the constraint answer set system clingcon, combining Answer Set Programming (ASP) with finite domain constraint processing (CP). While its predecessors rely on a black-box approach to h…
Grounding Recursive Aggregates: Preliminary Report
Problem solving in Answer Set Programming consists of two steps, a first grounding phase, systematically replacing all variables by terms, and a second solving phase computing the stable models of the obtained ground pro…