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.
| Verfasserangaben: | Pedro CabalarORCiDGND, Jorge FandinnoORCiD, Yuliya LierlerORCiDGND |
|---|---|
| DOI: | https://doi.org/10.1017/S1471068420000265 |
| ISSN: | 1471-0684 |
| ISSN: | 1475-3081 |
| Titel des übergeordneten Werks (Englisch): | Theory and practice of logic programming |
| Verlag: | Cambridge University Press |
| Verlagsort: | New York |
| Publikationstyp: | Wissenschaftlicher Artikel |
| Sprache: | Englisch |
| Datum der Erstveröffentlichung: | 21.09.2020 |
| Erscheinungsjahr: | 2020 |
| Datum der Freischaltung: | 20.09.2023 |
| Freies Schlagwort / Tag: | Answer Set Programming; formal specification; formal verification; modular logic programs |
| Band: | 20 |
| Ausgabe: | 5 |
| Aufsatznummer: | PII S1471068420000265 |
| Seitenanzahl: | 16 |
| Erste Seite: | 767 |
| Letzte Seite: | 782 |
| Fördernde Institution: | MINECO, Spain [TIN2017-84453-P]; NSF, USANational Science Foundation; (NSF) [1707371]; Alexander von Humboldt FoundationAlexander von Humboldt; Foundation |
| Organisationseinheiten: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Physik und Astronomie |
| DDC-Klassifikation: | 5 Naturwissenschaften und Mathematik / 53 Physik / 530 Physik |
| Peer Review: | Referiert |
