Proving completeness of logic programs with the cut
2017 (English)In: Formal Aspects of Computing, ISSN 0934-5043, E-ISSN 1433-299X, Vol. 29, no 1, 155-172 p.Article in journal (Refereed) Published
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 of completeness. This paper proposes a way of proving completeness of programs with the cut. The semantics of the cut is formalized by describing how SLD-trees are pruned. A sufficient condition for completeness is presented, proved sound, and illustrated by examples.
Place, publisher, year, edition, pages
SPRINGER , 2017. Vol. 29, no 1, 155-172 p.
Logic programming; The cut; Operational semantics; Program completeness; Program correctness
IdentifiersURN: urn:nbn:se:liu:diva-134608DOI: 10.1007/s00165-016-0392-0ISI: 000392128400007OAI: oai:DiVA.org:liu-134608DiVA: diva2:1075997