Inductive Theorem Proving meets Dependency Pairs

2010/01/01 by Stephan Swiderski, Swiderski, Stephan, Michael Parting +7
Computer Science · #Dependency Pairs #Inductive Theorem Proving #Logic, programming, and type systems #Natural Language Processing Techniques #Semantic Web and Ontologies #Term Rewriting #Termination

paper · doi:10.4230/dagsemproc.09411.4

openalex publication_date 2010/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for TRS termination with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.

Related

• Proving and Disproving Termination in the Dependency Pair Framework
• A Dependency Pair Framework for Relative Termination of Term Rewriting
• Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
• Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting (Short WST Version)
• A static higher-order dependency pair framework