Verifying Tight Logic Programs with anthem and vampire

DOI10.1017/S1471068420000344MaRDI QIDQ5140011zbMATH OpenFDO

Authors Jorge Fandinno, Vladimir Lifschitz, Patrick Lühne, Torsten Schaub

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.02025

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60) Basic properties of first-order languages and structures (03C07)

Abstract: This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas. Under consideration for acceptance in TPLP.

Recommendations

• Verification of logic programs
• scientific article; zbMATH DE number 1975609
• A new technique for verifying and correcting logic programs
• scientific article; zbMATH DE number 1973214
• A proof-theoretic approach to the static analysis of logic programs
• Assertion based inductive verification methods for logic programs
• scientific article; zbMATH DE number 1497823
• Abstract interpretation based verification of logic programs
• Towards Verifying Logic Programs in the Input Language of clingo

Cites work

• A Translation-based Approach to the Verification of Modular Equivalence
• Abstract gringo
• Connecting first-order ASP and the logic FO(ID) through reducts
• Infinitary equilibrium logic and strongly equivalent logic programs
• Logic Programming and Nonmonotonic Reasoning
• Program completion in the input language of GRINGO
• Stable models and circumscription
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Tight logic programs
• Towards Verifying Logic Programs in the Input Language of clingo
• Verifying strong equivalence of programs in the input language of \textsc{gringo}

Cited in

(15)

• External behavior of a logic program and verification of refactoring
• On program completion, with an application to the sum and product puzzle
• Constraint answer set programming: integrational and translational (or SMT-based) approaches
• Synthesizing strongly equivalent logic programs: Beth definability for answer set programs via Craig interpolation in first-order logic
• Here and There with Arithmetic
• Verification for ASP denotational semantics: a case study using the PVS theorem prover
• Testing in ASP: revisited language and programming environment
• Transforming gringo rules into formulas in a natural way
• Verifying strong equivalence of programs in the input language of \textsc{gringo}
• Arguing correctness of ASP programs with aggregates
• Generalizing the syntax of terms in mini-\textsc{gringo}
• Program completion in the input language of GRINGO
• From felicitous models to answer set programming
• Semantics for conditional literals via the SM operator
• On Heuer's procedure for verifying strong equivalence

Describes a project that uses

Uses Software

• anthem
• Gringo
• TPTP
• VAMPIRE

This page was built for publication: Verifying Tight Logic Programs with anthem and vampire

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