TY - GEN
T1 - Extending the 2D dependency pair framework for conditional term rewriting systems
AU - Lucas, Salvador
AU - Meseguer, José
AU - Gutiérrez, Raúl
N1 - Partially supported by NSF grant CNS 13-19109, EU (FEDER), Spanish MINECO projects TIN2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and GV project PROMETEO/2011/052. Salvador Lucas’ research was developed during a sabbatical year at the UIUC and was also supported by GV grant BEST/2014/026. Raúl Gutiérrez is also supported by Juan de la Cierva Fellowship JCI-2012-13528.
PY - 2015
Y1 - 2015
N2 - Recently, a new dependency pair framework for proving operational termination of Conditional Term Rewriting Systems (CTRSs) has been introduced. We call it 2D Dependency Pair (DP) Framework for CTRSs because it makes explicit and exploits the bidimensional nature of the termination behavior of conditional rewriting, where rewriting steps s → t and rewritings s →∗ t (in zero or more steps) are defined for specific terms s and t by using an inference system where appropriate proof trees should be exhibited for such particular goals. In this setting, the horizontal component of the termination behavior concerns the existence of infinite sequences of rewriting steps, and the vertical component captures infinitely many climbs during the development of a proof tree for a single rewriting step. In this paper we extend the 2D DP Framework for CTRSs with several powerful processors for proving and disproving operational termination that specifically exploit the structure of conditional rules.We provide the first implementation of the 2D DP Framework as part of the termination tool mu-term. Our benchmarks suggest that, with our new processors, the 2D DP Framework is currently the most powerful technique for proving operational termination of CTRSs.
AB - Recently, a new dependency pair framework for proving operational termination of Conditional Term Rewriting Systems (CTRSs) has been introduced. We call it 2D Dependency Pair (DP) Framework for CTRSs because it makes explicit and exploits the bidimensional nature of the termination behavior of conditional rewriting, where rewriting steps s → t and rewritings s →∗ t (in zero or more steps) are defined for specific terms s and t by using an inference system where appropriate proof trees should be exhibited for such particular goals. In this setting, the horizontal component of the termination behavior concerns the existence of infinite sequences of rewriting steps, and the vertical component captures infinitely many climbs during the development of a proof tree for a single rewriting step. In this paper we extend the 2D DP Framework for CTRSs with several powerful processors for proving and disproving operational termination that specifically exploit the structure of conditional rules.We provide the first implementation of the 2D DP Framework as part of the termination tool mu-term. Our benchmarks suggest that, with our new processors, the 2D DP Framework is currently the most powerful technique for proving operational termination of CTRSs.
KW - Conditional rewriting
KW - Dependency pairs
KW - Operational termination
KW - Program analysis
UR - http://www.scopus.com/inward/record.url?scp=84942540621&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84942540621&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-17822-6_7
DO - 10.1007/978-3-319-17822-6_7
M3 - Conference contribution
AN - SCOPUS:84942540621
SN - 9783319178219
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 113
EP - 130
BT - Logic-Based Program Synthesis and Transformation - 24th International Symposium, LOPSTR 2014, Revised Selected Papers
A2 - Proietti, Maurizio
A2 - Seki, Hirohisa
PB - Springer
T2 - 24th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2014
Y2 - 9 September 2014 through 11 September 2014
ER -