Modular Answer Set Programming as a formal specification language
- 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.
| Author details: | Pedro CabalarORCiDGND, Jorge FandinnoORCiD, Yuliya LierlerORCiDGND |
|---|---|
| DOI: | https://doi.org/10.1017/S1471068420000265 |
| ISSN: | 1471-0684 |
| ISSN: | 1475-3081 |
| Title of parent work (English): | Theory and practice of logic programming |
| Publisher: | Cambridge University Press |
| Place of publishing: | New York |
| Publication type: | Article |
| Language: | English |
| Date of first publication: | 2020/09/21 |
| Publication year: | 2020 |
| Release date: | 2023/09/20 |
| Tag: | Answer Set Programming; formal specification; formal verification; modular logic programs |
| Volume: | 20 |
| Issue: | 5 |
| Article number: | PII S1471068420000265 |
| Number of pages: | 16 |
| First page: | 767 |
| Last Page: | 782 |
| Funding institution: | MINECO, Spain [TIN2017-84453-P]; NSF, USANational Science Foundation; (NSF) [1707371]; Alexander von Humboldt FoundationAlexander von Humboldt; Foundation |
| Organizational units: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Physik und Astronomie |
| DDC classification: | 5 Naturwissenschaften und Mathematik / 53 Physik / 530 Physik |
| Peer review: | Referiert |
