Proving termination properties of prolog programs: A semantic approach

AbstractIn this paper, we define a framework in which the termination of Prolog programs can be proved. This framework relies on a semantics of Prolog that takes Prolog's control into account. A major asset of the method is that it makes the proof of termination (and other) properties of Prolog programs possible within a classical first-order logic setting