In this paper, we define two particular forms of non-termination, namely loops and binary chains, in an abstract framework that encompasses term rewriting and logic programming. The definition of loops relies on the notion of compatibility of binary relations. We also present a syntactic criterion for the detection of a special case of binary chains. Moreover, we describe our implementation NTI and compare its results at the Termination Competition 2023 with those of leading analyzers.

翻译：本文在涵盖术语重写与逻辑编程的抽象框架中，定义了两种特殊的非终止形态，即循环与二元链。循环的定义基于二元关系的相容性概念。同时，我们提出了一个用于检测二元链特例的句法准则。此外，我们描述了所实现的工具NTI，并将其在2023年终止竞赛中的表现与主流分析器进行了比较。