Correctness and Completeness of Logic Programs
2016 (English)In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 17, no 3, 18Article in journal (Refereed) Published
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.
Place, publisher, year, edition, pages
ACM Special Interest Group on Computer Science Education, 2016. Vol. 17, no 3, 18
logic programming, declarative programming, program completeness, program correctness, specifications, declarative diagnosis/algorithmic debugging
IdentifiersURN: urn:nbn:se:liu:diva-130237DOI: 10.1145/2898434ISI: 000380019200004OAI: oai:DiVA.org:liu-130237DiVA: diva2:949760