TY  - JOUR
A1  - Cabalar, Pedro
A1  - Fandinno, Jorge
A1  - Lierler, Yuliya
T1  - Modular Answer Set Programming as a formal specification language
T2  - Theory and practice of logic programming
N2  - In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining aformal proofshowing that the answer sets of a given (non-ground) logic programPcorrectly correspond to the solutions to the problem encoded byP, 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 modulesthat may incorporate local hidden atoms at different levels. Then,verifyingthe logic programPamounts to prove some kind of equivalence betweenPand its modular specification.
KW  - Answer Set Programming
KW  - formal specification
KW  - formal verification
KW  - modular logic programs
Y1  - 2020
UR  - https://publishup.uni-potsdam.de/frontdoor/index/index/docId/60772
SN  - 1471-0684
SN  - 1475-3081
VL  - 20
IS  - 5
SP  - 767
EP  - 782
PB  - Cambridge University Press
CY  - New York
ER  -