Verification for ASP denotational semantics: a case study using the PVS theorem prover
Felicidad Aguado, Pablo Ascariz, Pedro Cabalar, Gilberto Pérez, Concepción Vidal · Logic Journal of IGPL · 2016
In this article, we present an encoding of the (recently proposed) denotational semantics for Answer Set Programming (ASP) and its monotonic basis into the input language of the theorem prover PVS. Using some libraries and features from PVS, we have obtained semi-automated proofs for several fundamental properties of ASP. In this way, to the best of our knowledge, we provide the first known application of formal verification to ASP.