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

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(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: Modular Answer Set Programming as a Formal Specification Language

Abstract: In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, 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 modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP.
Comments: Paper presented at the 36th International Conference on Logic Programming (ICLP 2019), University Of Calabria, Rende (CS), Italy, September 2020, 16 pages
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI)
Journal reference: Theory and Practice of Logic Programming 20 (2020) 767-782
DOI: 10.1017/S1471068420000265
Cite as: arXiv:2008.02015 [cs.LO]
  (or arXiv:2008.02015v2 [cs.LO] for this version)

Submission history

From: Jorge Fandinno [view email]
[v1] Wed, 5 Aug 2020 09:25:51 GMT (121kb)
[v2] Fri, 7 Aug 2020 09:40:40 GMT (102kb)

Link back to: arXiv, form interface, contact.