Inductive Theorem Proving meets Dependency Pairs

Interaction versus Automation: The two Faces of Deduction

计算机科学;物理学

S. Swiderski ; M. Parting ; J. Giesl ; C. Fuhs LuFG Informatik 2

PID  :  80101

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

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 one of the most popular techniques for TRS termination (the dependency pair method) with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are