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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,440

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.
Theorem proving for untyped constructive λ-calculus: implementation and application.A. Ramsay - 2001 - Logic Journal of the IGPL 9 (1):83-100.
Do we need models?Philip Hugly & Charles Sayward - 1987 - Notre Dame Journal of Formal Logic 28 (3):414-422.
System description: { A higher-order theorem prover?Michael Kohlhase - manuscript
Axiomatization of a Denotational Semantics for First-order Logic.C. Vermeulen - 2004 - Logic Journal of the IGPL 12 (4):277-299.
Metamathematics, machines, and Gödel's proof.N. Shankar - 1994 - New York: Cambridge University Press.
Program verification within and without logic.Hajnal Andreka, Istvan Nemeti & Ildiko Sain - 1979 - Bulletin of the Section of Logic 8 (3):124-128.
Theorem Proving and Model Building with the Calculus KE.Jeremy Pitt & Jim Cunningham - 1996 - Logic Journal of the IGPL 4 (1):129-150.
Implementing a relational theorem prover for modal logic K.Angel Mora, Emilio Munoz Velasco & Joanna Golińska-Pilarek - 2011 - International Journal of Computer Mathematics 88 (9):1869-1884.
A Completeness Theorem For Symmetric Product Phase Spaces.Thomas Ehrhard - 2004 - Journal of Symbolic Logic 69 (2):340-370.
Interest driven suppositional reasoning.John Pollock - manuscript
Automated Theorem Proving and Its Prospects. [REVIEW]Desmond Fearnley-Sander - 1995 - PSYCHE: An Interdisciplinary Journal of Research On Consciousness 2.
Mlp: String-Functional Semantics and Boyer-Moore Mechanization for the Formal Verification of Synchronous Circuits.Alexandre Bronstein - 1990 - Dissertation, Stanford University
Foundations of a theorem prover for functional and mathematical uses.Javier Leach & Susana Nieva - 1993 - Journal of Applied Non-Classical Logics 3 (1):7-38.
Deepening the Automated Search for Gödel's Proofs.Adam Conkey - unknown

Analytics

Added to PP
2018-01-06

Downloads
2 (#1,809,250)

6 months
1 (#1,478,912)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Gustavo Gómez Pérez
Pontifical Javeriana University

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references