The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors
作者：
Highlights：
• We define a 2D Dependency Pair Framework to mechanically prove and disprove termination properties of CTRSs.
• We introduce several processors for their use in the 2D DP Framework.
• Implemented as part of the termination tool mu-term.
• Proved its power in the International Termination Competition.
• In a forthcoming second part we will introduce other processors and provide implementation details.
摘要
•We define a 2D Dependency Pair Framework to mechanically prove and disprove termination properties of CTRSs.•We introduce several processors for their use in the 2D DP Framework.•Implemented as part of the termination tool mu-term.•Proved its power in the International Termination Competition.•In a forthcoming second part we will introduce other processors and provide implementation details.
论文关键词：Conditional term rewriting,Dependency pairs,Program analysis,Operational termination
论文评审过程：Received 18 April 2016, Revised 12 April 2018, Accepted 13 April 2018, Available online 25 April 2018, Version of Record 31 May 2018.
论文官网地址：https://doi.org/10.1016/j.jcss.2018.04.002
