Advertisement
Published in:
2005 | OriginalPaper | Chapter
Orderings for Innermost Termination
Authors : Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio
Published in: Term Rewriting 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
This paper shows that the suitable orderings for proving innermost termination are characterized by the
innermost parallel monotonicity
,
IP-monotonicity
for short. This property may lead to several innermost-specific orderings. Here, an IP-monotonic version of the
Recursive Path Ordering
is presented. This variant can be used (directly or as ingredient of the
Dependency Pairs
method) for proving innermost termination of non-terminating term rewrite systems.