Non-Termination in Term Rewriting and Logic Programming
Logic in Computer Science
2023-12-22 v1
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.
Keywords
Cite
@article{arxiv.2312.13949,
title = {Non-Termination in Term Rewriting and Logic Programming},
author = {Etienne Payet},
journal= {arXiv preprint arXiv:2312.13949},
year = {2023}
}
Comments
Accepted for publication in Journal of Automated Reasoning, December 2023