Proving completeness of logic programs with the cut

TL;DR

This paper introduces a formal method to prove the completeness of Prolog programs that use the cut, by modeling how the cut prunes search trees and establishing conditions for maintaining completeness.

Contribution

It formalizes the semantics of the cut in Prolog and provides a sound, sufficient condition for proving program completeness involving the cut.

Findings

A formal semantics for the cut's pruning effect.

A sound, sufficient condition for completeness with the cut.

Illustrative examples demonstrating the proof method.

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.