Binary Non-Termination in Term Rewriting and Logic Programming

TL;DR

This paper introduces a new syntactic method for automatically detecting non-termination in simplified models of term rewriting and logic programming, aiding in program analysis.

Contribution

It proposes a novel syntactic criterion that generalizes non-termination detection across term rewriting and logic programming.

Findings

Effective in identifying non-termination cases

Applicable to a broad class of rewriting and logic programs

Simplifies non-termination analysis process

Abstract

We present a new syntactic criterion for the automatic detection of non-termination in an abstract setting that encompasses a simplified form of term rewriting and logic programming.