Verifying tight logic programs with Anthem and Vampire
- This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.
| Author details: | Jorge FandinnoORCiD, Vladimir LifschitzORCiDGND, Patrick LühneORCiD, Torsten H. SchaubORCiDGND |
|---|---|
| DOI: | https://doi.org/10.1017/S1471068420000344 |
| ISSN: | 1471-0684 |
| ISSN: | 1475-3081 |
| Title of parent work (English): | Theory and practice of logic programming |
| Publisher: | Cambridge Univ. Press |
| Place of publishing: | Cambridge [u.a.] |
| Publication type: | Article |
| Language: | English |
| Date of first publication: | 2020/09/21 |
| Publication year: | 2020 |
| Release date: | 2023/06/02 |
| Volume: | 20 |
| Issue: | 5 |
| Number of pages: | 16 |
| First page: | 735 |
| Last Page: | 750 |
| Funding institution: | Alexander von Humboldt Foundation |
| Organizational units: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science |
| DDC classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 000 Informatik, Informationswissenschaft, allgemeine Werke |
| Peer review: | Referiert |
