Modular Answer Set Programming as a Formal Specification Language. Issue 5 (September 2020)

• Record Type: Journal Article
• Authors: CABALAR, PEDRO; FANDINNO, JORGE; LIERLER, YULIYA
• Is Part Of: Theory and practice of logic programming. Volume 20:Issue 5(2020)
• Page Start: 767
• Page End: 782
• Publication Date: 2020-09
• Subjects: Answer Set Programming, -- Formal Specification, -- Formal Verification, -- Modular Logic Programs; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068420000265
• Languages: English
• ISSNs: 1471-0684

Abstract

Abstract: 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.