Related papers: Verification of Locally Tight Programs
Completion is a well-known transformation that captures the stable model semantics of logic programs by turning a program into a set of first-order definitions. Stable models are models of the completion, but not all models of the…
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…
In a recent paper by Harrison et al., the concept of program completion is extended to a large class of programs in the input language of the ASP grounder gringo. We would like to automate the process of generating and simplifying…
This note is about the relationship between two theories of negation as failure -- one based on program completion, the other based on stable models, or answer sets. Francois Fages showed that if a logic program satisfies a certain…
Program correctness (in imperative and functional programming) splits in logic programming into correctness and completeness. Completeness means that a program produces all the answers required by its specification. Little work has been…
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…
Program verification is to develop the program's proof system, and to prove the proof system soundness with respect to a trusted operational semantics of the program. However, many practical program verifiers are not based on operational…
With the increase in industrial applications using Answer Set Programming, the need for formal verification tools, particularly for critical applications, has also increased. During the program optimisation process, it would be desirable to…
We present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for…
We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our…
The term {\em meta-programming} refers to the ability of writing programs that have other programs as data and exploit their semantics. The aim of this paper is presenting a methodology allowing us to perform a correct termination analysis…
An approximate program transformation is a transformation that can change the semantics of a program within a specified empirical error bound. Such transformations have wide applications: they can decrease computation time, power…
There are many different semantics for general logic programs (i.e. programs that use negation in the bodies of clauses). Most of these semantics are Turing complete (in a sense that can be made precise), implying that they are undecidable.…
`What more than its truth do we know if we have a proof of a theorem in a given formal system?' We examine Kreisel's question in the particular context of program termination proofs, with an eye to deriving complexity bounds on program…
Answer Set Programming (ASP) is an important logic programming paradigm within the field of Knowledge Representation and Reasoning. As a concise, human-readable, declarative language, ASP is an excellent tool for developing trustworthy…
We introduce a method of verifying termination of logic programs with respect to concrete queries (instead of abstract query patterns). A necessary and sufficient condition is established and an algorithm for automatic verification is…
Anthem 2.0 is a tool to aid in the verification of logic programs written in an expressive fragment of Clingo's input language named mini-gringo, which includes arithmetic operations and simple choice rules but not aggregates. It can…
This paper describes a generalization of Clark's completion that is applicable to logic programs containing arithmetic operations and produces syntactically simple, natural looking formulas. If a set of first-order axioms is equivalent to…
We argue that turning a logic program into a set of completed definitions can be sometimes thought of as the "reverse engineering" process of generating a set of conditions that could serve as a specification for it. Accordingly, it may be…
{log} (read 'setlog') was born as a Constraint Logic Programming (CLP) language where sets and binary relations are first-class citizens, thus fostering set programming. Internally, {log} is a constraint satisfiability solver implementing…