Refine
Has Fulltext
- no (1)
Year of publication
- 2020 (1)
Document Type
- Article (1)
Language
- English (1)
Is part of the Bibliography
- yes (1) (remove)
Keywords
- formal verification (1) (remove)
Institute
- Institut für Physik und Astronomie (1) (remove)
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.