The Dependency Triple Framework for Termination of Logic Programs

We show how to combine the two most powerful approaches for automated termination analysis of logic programs (LPs): the direct approach which operates directly on LPs and the transformational approach which transforms LPs to term rewrite systems (TRSs) and tries to prove termination of the resulting TRSs. To this end, we adapt the well-known dependency pair framework from TRSs to LPs. With the resulting method, one can combine arbitrary termination techniques for LPs in a completely modular way and one can use both direct and transformational techniques for different parts of the same LP.

• Type: Conference
• Year: 2009
• Where: LOPSTR
• Authors: Peter Schneider-Kamp, Jürgen Giesl, Manh Thang Nguyen
• Keywords: Arbitrary Termination Techniques, Artificial Intelligence, LOPSTR 2009, Termination Analysis, Well-known Dependency Pair