Verifying Termination of General Logic Programs with Concrete Queries

TL;DR

This paper presents a new, automated method for verifying the termination of general logic programs with concrete queries, unifying termination analysis and loop checking without complex computations.

Contribution

It introduces a necessary and sufficient condition for termination verification applicable to all non-floundering logic programs, simplifying automation and bridging two previously separate analysis problems.

Findings

Applicable to all non-floundering logic programs

Does not require level mappings or mode/type info

Unifies termination analysis with loop checking

Abstract

We introduce a method of verifying termination of logic programs with respect to concrete queries (instead of abstract query patterns). A necessary and sufficient condition is established and an algorithm for automatic verification is developed. In contrast to existing query pattern-based approaches, our method has the following features: (1) It applies to all general logic programs with non-floundering queries. (2) It is very easy to automate because it does not need to search for a level mapping or a model, nor does it need to compute an interargument relation based on additional mode or type information. (3) It bridges termination analysis with loop checking, the two problems that have been studied separately in the past despite their close technical relation with each other.