Journal Articles Journal of Automated Reasoning Year : 2024

Non-termination in Term Rewriting and Logic Programming

Abstract

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.

Dates and versions

hal-04436108 , version 1 (03-02-2024)

Identifiers

Cite

Etienne Payet. Non-termination in Term Rewriting and Logic Programming. Journal of Automated Reasoning, 2024, 68 (4), pp.24. ⟨10.1007/s10817-023-09693-z⟩. ⟨hal-04436108⟩
35 View
0 Download

Altmetric

Share

More