liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Correctness and Completeness of Logic Programs
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering. Institute of Computer Science, Polish Academy of Sciences, Warzawa, Poland.ORCID iD: 0000-0002-4700-7272
2016 (English)In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 17, no 3, 18Article in journal (Refereed) Published
Abstract [en]

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
Keyword [en]
logic programming, declarative programming, program completeness, program correctness, specifications, declarative diagnosis/algorithmic debugging
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:liu:diva-130237DOI: 10.1145/2898434ISI: 000380019200004OAI: oai:DiVA.org:liu-130237DiVA: diva2:949760
Available from: 2016-07-23 Created: 2016-07-23 Last updated: 2016-09-19Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Drabent, Włodzimierz
By organisation
Software and SystemsFaculty of Science & Engineering
In the same journal
ACM Transactions on Computational Logic
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 35 hits
ReferencesLink to record
Permanent link

Direct link