Modular answer set programming as a formal specification language

DOI10.1017/S1471068420000265MaRDI QIDQ5140013zbMATH OpenFDO

Authors Pedro Cabalar, Jorge Fandinno, Yuliya Lierler

Publication date 13 December 2020

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2008.02015

zbMATH Keywords

answer-set programmingformal specificationformal verificationmodular logic programs

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP.

Recommendations

• Verification for ASP denotational semantics: a case study using the PVS theorem prover
• A Translation-based Approach to the Verification of Modular Equivalence
• Modular nonmonotonic logic programming revisited
• Model Checking Abstract State Machines with Answer Set Programming
• Modules and specifications

Cites work

• A Characterization of Strong Equivalence for Logic Programs with Variables
• A Tarskian informal semantics for answer set programming
• A Translation-based Approach to the Verification of Modular Equivalence
• Achievements in answer set programming
• Characterising relativised strong equivalence with projection for non-ground answer-set programs
• Conflict-Driven Answer Set Enumeration
• First-order modular logic programs and their conservative extensions
• Forgetting auxiliary atoms in forks
• scientific article; zbMATH DE number 1368933 (Why is no real title available?)
• scientific article; zbMATH DE number 1909430 (Why is no real title available?)
• scientific article; zbMATH DE number 5212421 (Why is no real title available?)
• Logic Programming and Nonmonotonic Reasoning
• Logic programs with propositional connectives and aggregates
• Logic programs with stable model semantics as a constraint programming paradigm
• Modular answer set programming as a formal specification language
• Performance tuning in answer set programming
• Program Correspondence under the Answer-Set Semantics: The Non-ground Case
• Quantified Equilibrium Logic and Foundations for Answer Set Programs
• Stable models and circumscription
• Strongly equivalent logic programs
• You can't always forget what you want: on the limits of forgetting in answer set programming

Cited in

(10)

• Uhura: an authoring tool for specifying answer-set programs using controlled natural language
• Answer set programming with graded modality
• Arguing correctness of ASP programs with aggregates
• Semantics for conditional literals via the SM operator
• A Translation-based Approach to the Verification of Modular Equivalence
• Verification for ASP denotational semantics: a case study using the PVS theorem prover
• Modular answer set programming as a formal specification language
• Using answer set programming in the development of verified software
• Macros, Macro Calls and Use of Ensembles in Modular Answer Set Programming
• Constraint answer set programming: integrational and translational (or SMT-based) approaches

Describes a project that uses

Uses Software

• anthem

This page was built for publication: Modular answer set programming as a formal specification language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5140013)