cTI: A constraint-based termination inference tool for ISO-Prolog

TL;DR

cTI is a novel system that automatically infers classes of queries for which logic programs, specifically ISO-Prolog, terminate, eliminating the need for user annotations and reanalysis when query classes change.

Contribution

The paper introduces cTI, the first universal left-termination inference tool for logic programs, enabling automatic inference of terminating query classes without user input.

Findings

Successfully inferred terminating classes for various classical logic programs.

Demonstrated effectiveness on large and complex Prolog programs.

Outperformed traditional termination analyzers in flexibility and coverage.

Abstract

We present cTI, the first system for universal left-termination inference of logic programs. Termination inference generalizes termination analysis and checking. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided to the system, for instance by means of user annotations. Moreover, the analysis must be redone every time the class of queries of interest is updated. Termination inference, in contrast, requires neither user annotations nor recomputation. In this approach, terminating classes for all predicates are inferred at once. We describe the architecture of cTI and report an extensive experimental evaluation of the system covering many classical examples from the logic programming termination literature and several Prolog programs of respectable size and complexity.