Non-termination Analysis of Logic Programs with Integer arithmetics

TL;DR

This paper introduces a non-termination analysis method for logic programs with integer arithmetic, extending previous analyzers to handle real-world Prolog programs by modeling arithmetic constraints.

Contribution

It presents a novel non-termination condition specifically for logic programs with integer arithmetic, building on prior analyzers and addressing practical Prolog features.

Findings

The analyzer can identify non-terminating queries involving integer arithmetic.

It models arithmetic success as a constraint problem to improve analysis accuracy.

The approach extends existing analyzers to more realistic Prolog programs.

Abstract

In the past years, analyzers have been introduced to detect classes of non-terminating queries for definite logic programs. Although these non-termination analyzers have shown to be rather precise, their applicability on real-life Prolog programs is limited because most Prolog programs use non-logical features. As a first step towards the analysis of Prolog programs, this paper presents a non-termination condition for Logic Programs containing integer arithmetics. The analyzer is based on our non-termination analyzer presented at ICLP 2009. The analysis starts from a class of queries and infers a subclass of non-terminating ones. In a first phase, we ignore the outcome (success or failure) of the arithmetic operations, assuming success of all arithmetic calls. In a second phase, we characterize successful arithmetic calls as a constraint problem, the solution of which determines the non-terminating queries.