Loading...
Please wait, while we are loading the content...
Similar Documents
Proving correctness and completeness of normal programs – a declarative approach
| Content Provider | Scilit |
|---|---|
| Author | Drabent, Włodzimierz Miłkowska, Mirosława |
| Copyright Year | 2005 |
| Description | 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 operational semantics, in particular on the selection rule. We show how to deal with correctness and completeness in a declarative way, treating programs only from the logical point of view. Specifications used in this approach are interpretations (or theories). We point out that specifications for correctness may differ from those for completeness, as usually there are answers which are neither considered erroneous nor required to be computed. We present proof methods for correctness and completeness for definite programs and generalize them to normal programs. For normal programs we use the 3-valued completion semantics; this is a standard semantics corresponding to negation as finite failure. The proof methods employ solely the classical 2-valued logic. We use a 2-valued characterization of the 3-valued completion semantics, which may be of separate interest. The method of proving correctness of definite programs is not new and can be traced back to the work of clark in 1979. However a more complicated approach using operational semantics was proposed by some authors. We show that it is not stronger than the declarative one, as far as properties of program answers are concerned. For a corresponding operational approach to normal programs, we show that it is (strictly) weaker than our method. We also employ the ideas of this work to generalize a known method of proving termination of normal programs. |
| Related Links | http://arxiv.org/pdf/cs/0501043 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/C331F9C364AD2E5C9B3BEDD01AFA70D1/S147106840500253Xa.pdf/div-class-title-proving-correctness-and-completeness-of-normal-programs-a-declarative-approach-div.pdf |
| Ending Page | 711 |
| Page Count | 43 |
| Starting Page | 669 |
| ISSN | 14710684 |
| e-ISSN | 14753081 |
| DOI | 10.1017/s147106840500253x |
| Journal | Theory and Practice of Logic Programming |
| Issue Number | 6 |
| Volume Number | 5 |
| Language | English |
| Publisher | Cambridge University Press (CUP) |
| Publisher Date | 2005-11-01 |
| Access Restriction | Open |
| Subject Keyword | Theory and Practice of Logic Programming History and Philosophy of Science Declarative Programming Negation in Logic Programming Program Correctness and Completeness Teaching Logic Programming |
| Content Type | Text |
| Resource Type | Article |
| Subject | Artificial Intelligence Theoretical Computer Science Computational Theory and Mathematics Hardware and Architecture Software |
