Tallahassee, Florida, United States of America
  •  1
    Verification for ASP denotational semantics: A case study using the PVS theorem prover
    with F. Aguado, P. Ascariz, P. Cabalar, and C. Vidal
    Logic Journal of the IGPL 25 (2): 195-213. 2017.
    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.