SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
summary
Proposes an SM-based semantics for answer set programs with conditional literals and integer arithmetic that avoids grounding by extending the toar translation and applying the SM operator, proves via Proposition 2 and Theorem 1 that this characterization is strongly equivalent to clingo’s infinitary semantics, implements the approach in Anthem (Rust + Vampire) and uses it to automatically verify examples (choice/conditional refactor and graph‑coloring external equivalence), and reports that the implementation successfully automates the intended strong‑ and external‑equivalence checks.
AI-written summary · about
chapters (10)
- 0:00SM-based ASP semantics intro
- 2:55ASP rules and conditional literals
- 8:12HT and equilibrium logic
- 10:24Extending mini Gringo
- 13:40Conditional literals to first-order logic
- 14:23SM operator for stable models
- 16:11Proposed answer set semantics
- 18:17Anthem tool implementation
- 19:42Paper contributions and future work
- 20:34Q&A
related talks
30mAnalyzing Programs with SMT Solvers
20mCertified Abstract Machines for Skeletal Semantics
22mMechanised Semantics for Gated Static Single Assignment
12mContextual Algebraic Theories: Generic Boilerplate beyond Abstraction
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
30mSemantics-Guided Synthesis
16mS4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
18mCertified Semantics for Disequality