TY - GEN
T1 - Dealing with non-orientable equations in rewriting induction
AU - Aoto, Takahito
PY - 2006/1/1
Y1 - 2006/1/1
N2 - Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order. Thus, when the given conjecture is not orientable by the reduction order in use, any proof attempts for that conjecture fails; also conjectures such as a commutativity equation are out of the scope of the rewriting induction because they can not be oriented by any reduction order. In this paper, we give an enhanced rewriting induction which can deal with non-orientable conjectures. We also present an extension which intends an incremental use of our enhanced rewriting induction.
AB - Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order. Thus, when the given conjecture is not orientable by the reduction order in use, any proof attempts for that conjecture fails; also conjectures such as a commutativity equation are out of the scope of the rewriting induction because they can not be oriented by any reduction order. In this paper, we give an enhanced rewriting induction which can deal with non-orientable conjectures. We also present an extension which intends an incremental use of our enhanced rewriting induction.
UR - http://www.scopus.com/inward/record.url?scp=33749402649&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33749402649&partnerID=8YFLogxK
U2 - 10.1007/11805618_18
DO - 10.1007/11805618_18
M3 - Conference contribution
AN - SCOPUS:33749402649
SN - 3540368345
SN - 9783540368342
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 242
EP - 256
BT - Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings
PB - Springer Verlag
T2 - 17th International Conference on Term Rewriting and Applications, RTA 2006
Y2 - 12 August 2006 through 14 August 2006
ER -