Automated Termination Analysis for Logic Programs with Cut

TL;DR

This paper presents a new pre-processing technique that transforms Prolog programs with cut into cut-free logic programs, enabling existing termination analysis methods to verify termination properties effectively.

Contribution

It introduces a novel automatic transformation method for Prolog programs with cut, integrating it into the AProVE termination prover for improved analysis.

Findings

Successfully implemented in AProVE

Effective in handling real-world Prolog programs

Enables existing techniques to analyze cut-containing programs

Abstract

Termination is an important and well-studied property for logic programs. However, almost all approaches for automated termination analysis focus on definite logic programs, whereas real-world Prolog programs typically use the cut operator. We introduce a novel pre-processing method which automatically transforms Prolog programs into logic programs without cuts, where termination of the cut-free program implies termination of the original program. Hence after this pre-processing, any technique for proving termination of definite logic programs can be applied. We implemented this pre-processing in our termination prover AProVE and evaluated it successfully with extensive experiments.