Related papers: Correctness and completeness of logic programs
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…
Completeness of a logic program means that the program produces all the answers required by its specification. The cut is an important construct of programming language Prolog. It prunes part of the search space, this may result in a loss…
We advocate a declarative approach to proving properties of logic programs. Total correctness can be separated into correctness, completeness and clean termination; the latter includes non-floundering. Only clean termination depends on the…
Partial correctness of imperative or functional programming divides in logic programming into two notions. Correctness means that all answers of the program are compatible with the specification. Completeness means that the program produces…
This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic…
It is well known that the resolution method (for propositional logic) is complete. However, completeness proofs found in the literature use an argument by contradiction showing that if a set of clauses is unsatisfiable, then it must have a…
The programming language Prolog makes declarative programming possible, at least to a substantial extent. Programs may be written and reasoned about in terms of their declarative semantics. All the advantages of declarative programming are…
Logic languages based on the theory of rational, possibly infinite, trees have much appeal in that rational trees allow for faster unification (due to the safe omission of the occurs-check) and increased expressivity (cyclic terms can…
In solving a query, the SLD proof procedure for definite programs sometimes searches an infinite space for a non existing solution. For example, querying a planner for an unreachable goal state. Such programs motivate the development of…
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.…
Tabled logic programming is receiving increasing attention in the Logic Programming community. It avoids many of the shortcomings of SLD execution and provides a more flexible and often extremely efficient execution mechanism for logic…
Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning,…
This paper describes a general framework for automatic termination analysis of logic programs, where we understand by ``termination'' the finitenes s of the LD-tree constructed for the program and a given query. A general property of…
Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles…
We present verification methods for logic programs with delay declarations. The verified properties are termination and freedom from errors related to built-ins. Concerning termination, we present two approaches. The first approach tries to…
Thom Fr\"uhwirth presented a short, elegant and efficient Prolog program for the n queens problem. However the program may be seen as rather tricky and one may not be convinced about its correctness. This paper explains the program in a…
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…
Many logic programming based approaches can be used to describe and solve combinatorial search problems. On the one hand there are definite programs and constraint logic programs that compute a solution as an answer substitution to a query…
We propose a modular method for proving termination of general logic programs (i.e., logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider…
We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a…