Advertisement
Published in:
2008 | OriginalPaper | Chapter
Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
Author : Sorin Stratulat
Published in: Rewriting Techniques and Applications
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We propose a new (Noetherian) induction schema to reason on equalities and show how to integrate it into implicit induction-based inference systems. Non-orientable conjectures of the form
lhs
=
rhs
and their instances can be soundly used as induction hypotheses in rewrite operations. It covers the most important rewriting-based induction proof techniques: i)
term rewriting induction
if
lhs
=
rhs
is orientable, ii)
enhanced rewriting induction
if
lhs
and
rhs
are comparable, iii)
ordered rewriting induction
if the instances of
lhs
=
rhs
are orientable, and iv)
relaxed rewriting induction
if the instances of
lhs
=
rhs
are not comparable.In practice, it helps to automatize the (rewrite-based) reasoning on a larger class of non-orientable equalities, like the permutative and associativity equalities.