Modular Answer Set Programming as a Formal Specification Language

TL;DR

This paper introduces a formal specification language based on modular Answer Set Programming (ASP) to verify that logic programs correctly represent problem solutions, enhancing the reliability of ASP applications.

Contribution

It proposes a novel modular specification language for ASP, enabling formal verification of logic programs against their specifications using equivalence proofs.

Findings

Defines a new ASP module formalism with nested and local atoms

Enables formal verification of ASP programs through modular equivalence

Facilitates isolated reasoning about problem aspects in ASP specifications

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.