Verifying Tight Logic Programs with anthem and Vampire

TL;DR

This paper extends the concept of program completion to input/output logic programs, analyzes their stable models, and demonstrates verification techniques using anthem and Vampire tools.

Contribution

It introduces a new approach to verify logic programs with input/output by extending completion definitions and relating them to stable models.

Findings

Extended program completion to input/output programs.

Established relationship between stable models and completion.

Performed preliminary verification experiments with anthem and Vampire.

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.