Article
Arguing Correctness of ASP Programs with Aggregates
Proceedings of the 16th International Conference on Logic Programming and Non-monotonic Reasoning
(2022)
Abstract
This paper studies the problem of arguing program correctness for logic programs with aggregates in the context of Answer Set Programming. Cabalar, Fandinno, and Lierler (2020) championed a modular methodology for arguing program correctness. We show how a recently proposed many-sorted semantics for logic programs with aggregates allows us to apply their methodology to this type of program. This is illustrated using well-known encodings for the Graph Coloring and Traveling Salesman problems. In particular, we showcase how this modular approach allows us to reuse the proof of correctness of a Hamiltonian Cycle encoding studied in a previous publication when considering the Traveling Salesman program.
Disciplines
Publication Date
2022
Citation Information
Jorge Fandinno, Zachary Hansen and Yuliya Lierler. "Arguing Correctness of ASP Programs with Aggregates" Proceedings of the 16th International Conference on Logic Programming and Non-monotonic Reasoning (2022) Available at: http://works.bepress.com/yuliya_lierler/116/