Verification for ASP denotational semantics: A case study using the PVS theorem prover

, , , &
Logic Journal of the IGPL 25 (2):195-213 (2017)
  Copy   BIBTEX

Abstract

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.

Categories

Keywords

Reprint years

DOI

10.1093/jigpal/jzw060

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,795

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

How to avoid the formal verification of a theorem prover.A. Avellone, M. Benini & U. Moscato - 2001 - Logic Journal of the IGPL 9 (1):1-25.
Answer-set programming encodings for argumentation frameworks.Uwe Egly, Sarah Alice Gaggl & Stefan Woltran - 2010 - Argument and Computation 1 (2):147-177.
A Completeness Theorem For Symmetric Product Phase Spaces.Thomas Ehrhard - 2004 - Journal of Symbolic Logic 69 (2):340-370.
On the relation between SPARQL1.1 and Answer Set Programming.Axel Polleres & Johannes Peter Wallner - 2013 - Journal of Applied Non-Classical Logics 23 (1-2):159-212.
RASP and ASP as a fragment of linear logic.Stefania Costantini & Andrea Formisano - 2013 - Journal of Applied Non-Classical Logics 23 (1-2):49-74.
Speedith: A Reasoner for Spider Diagrams.Matej Urbas, Mateja Jamnik & Gem Stapleton - 2015 - Journal of Logic, Language and Information 24 (4):487-540.
Deepening the Automated Search for Gödel's Proofs.Adam Conkey - unknown
Automated legal reasoning with discretion to act using s(LAW).Joaquín Arias, Mar Moreno-Rebato, Jose A. Rodriguez-García & Sascha Ossowski - 2024 - Artificial Intelligence and Law 32 (4):1141-1164.
Multimodal and intuitionistic logics in simple type theory.Christoph Benzmueller & Lawrence Paulson - 2010 - Logic Journal of the IGPL 18 (6):881-892.
What is answer set programming?Vladimir Lifschitz - unknown

Analytics

Added to PP
2018-01-06

Downloads
10 (#1,478,542)

6 months
4 (#1,269,568)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references