We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Verifying Tight Logic Programs with anthem and Vampire

Abstract: 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. Under consideration for acceptance in TPLP.
Comments: Paper submitted to the 36th International Conference on Logic Programming (ICLP 2020), University Of Calabria, Rende (CS), Italy, September 2020, 16 pages (main part), 12 pages (appendix)
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI)
Journal reference: Theory and Practice of Logic Programming 20 (2020) 735-750
DOI: 10.1017/S1471068420000344
Cite as: arXiv:2008.02025 [cs.LO]
  (or arXiv:2008.02025v5 [cs.LO] for this version)

Submission history

From: Jorge Fandinno [view email]
[v1] Wed, 5 Aug 2020 10:01:33 GMT (53kb)
[v2] Sun, 9 Aug 2020 23:32:54 GMT (51kb)
[v3] Tue, 11 Aug 2020 21:52:46 GMT (51kb)
[v4] Sat, 4 Sep 2021 14:56:05 GMT (51kb)
[v5] Mon, 18 Jul 2022 13:07:43 GMT (35kb)

Link back to: arXiv, form interface, contact.