Gabriel Baquero

In this article, we present an encoding of the denotational semantics for Answer Set Programming 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.

Creation mustn't be considerated as a production whose term is creature. Creature as such isn't a term but a beginning. Abandonment of mental limit is a necessary method to reach such a knowledge of creature