Partial Argument Filtering for Termination Analysis of Logic Programs

---

Automated termination analysis has become more and more relevant for practical use, even though the underlying problem is in general undecidable. This is particularly true for logic programming, since virtually all logic programs are non-terminating if one considers all possible queries. Thus, termination of logic programs is widely studied and significant advances have been made during the last decades. Nowadays, there are fully-automated tools that try to prove termination of a given logic program w.r.t. a given class of inputs. One of them is the termination prover AProVE which uses a transformational approach, i.e., AProVE transforms logic programs into term rewrite systems (TRSs) whose termination implies termination of the original logic program. In this talk, we improve the approach of AProVE such that we can now handle logic programs where regarding different “modings” of constructor symbols (e.g., list constructors) is essential in order to prove termination. To this end, we adapted the successful dependency pair framework to TRSs with start terms. Thus, we can investigate local termination and consider several modings for constructor symbols in different SCCs of the corresponding dependency graph. We implemented our improvements in AProVE and show an empirical comparison with the old system and the Narradar tool.