Correctness and completeness of logic programs
From MaRDI portal
Abstract: We discuss proving correctness and completeness of definite clause logic programs. We propose a method for proving completeness, while for proving correctness we employ a method which should be well known but is often neglected. Also, we show how to prove completeness and correctness in the presence of SLD-tree pruning, and point out that approximate specifications simplify specifications and proofs. We compare the proof methods to declarative diagnosis (algorithmic debugging), showing that approximate specifications eliminate a major drawback of the latter. We argue that our proof methods reflect natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming.
Recommendations
- On completeness of logic programs
- scientific article; zbMATH DE number 2085284
- Proving correctness and completeness of normal programs – a declarative approach
- Proof method of partial correctness and weak completeness for normal logic programs
- Logic + control: on program construction and verification
Cites work
- A pearl on SAT and SMT solving in Prolog
- A semantic basis for the termination analysis of logic programs
- A three-valued semantics for logic programmers
- Automated termination proofs for logic programs by term rewriting
- cTI: a constraint-based termination inference tool for ISO-Prolog
- scientific article; zbMATH DE number 3913653 (Why is no real title available?)
- scientific article; zbMATH DE number 3947593 (Why is no real title available?)
- scientific article; zbMATH DE number 3731310 (Why is no real title available?)
- scientific article; zbMATH DE number 1354157 (Why is no real title available?)
- scientific article; zbMATH DE number 708499 (Why is no real title available?)
- scientific article; zbMATH DE number 788036 (Why is no real title available?)
- Inductive assertion method for logic pograms
- Inferring non-suspension conditions for logic programs with dynamic scheduling
- Logic + control: an example
- Logic program synthesis
- Negation in logic programming
- On definite program answers and least Herbrand models
- Polytool: polynomial interpretations as a basis for termination analysis of logic programs
- Proving correctness and completeness of normal programs – a declarative approach
- Reasoning about termination of pure Prolog programs
- Strong termination of logic programs
- The relation between logic programming and logic specification
- The theoretical foundations of LPTP (a logic program theorem prover)
- The transformational approach to program development
- The well-founded semantics for general logic programs
- Truth versus information in logic programming
- XSB: extending Prolog with tabled logic programming
Cited in
(17)- On completeness of logic programs
- scientific article; zbMATH DE number 3856389 (Why is no real title available?)
- scientific article; zbMATH DE number 1223543 (Why is no real title available?)
- Correctness of unification without occur check in prolog
- On definite program answers and least Herbrand models
- Logic + control: on program construction and verification
- Completeness of a top-down declarative error diagnoser
- scientific article; zbMATH DE number 2085284 (Why is no real title available?)
- The Prolog debugger and declarative programming
- Proving completeness of logic programs with the cut
- Correctness of linear logic proof structures is NL-complete
- Logic + control: an example
- Proving correctness and completeness of normal programs – a declarative approach
- On Correctness and Completeness of an n Queens Program
- S-semantics -- an example
- On correctness of normal logic programs
- Strict completion of logic programs
This page was built for publication: Correctness and completeness of logic programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277919)
