Proving completeness of logic programs with the cut
Logic in Computer Science
2020-01-03 v1 Programming Languages
Abstract
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.
Cite
@article{arxiv.1602.08778,
title = {Proving completeness of logic programs with the cut},
author = {Włodzimierz Drabent},
journal= {arXiv preprint arXiv:1602.08778},
year = {2020}
}
Comments
17 pages