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.

You do not currently have access to this article.