Modular Answer Set Programming as a Formal Specification Language
This addresses the need for rigorous verification in ASP, which is incremental as it builds on existing ASP frameworks with a new modular approach.
The paper tackles the problem of formal verification for Answer Set Programming (ASP) by developing a modular specification language to prove that answer sets correctly encode problem solutions, regardless of instance, using novel nested modules with local hidden atoms.
In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP.