Campus Event Calendar

Event Entry

What and Who

Maximal Extensions of Simplification Orderings

Deepak Kapur
State University of New York at Albany
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS  
AG Audience

Date, Time and Location

Wednesday, 16 August 95
60 Minutes
44 - MPII


To show the termination of rewrite systems, several well-founded syntactic orderings have been proposed in the literature. While these orderings are total (up to equivalence) on ground terms, they are not maximal when used to compare non-ground terms, i.e., there can be two non-ground terms such that for all ground substitutions on them, first term is always bigger than the second term, but these orderings declare the two terms noncomparable. A new ordering based on paths is defined and and proved to be maximal. Recursive path orderings (RPO) are extended to define new families of orderings that are maximal. A construction of a maximal ordering is given by showing that given two terms s and t, it can be decided whether there is a ground substitution sigma that makes sigma(s) bigger than sigma(t) using RPO. A quadratic bound on the depth of a ground substitution required is established in terms of the depths of s and t. These results have interesting implications for constraint-based theorem proving.


Uwe Waldmann
(0681) 302-5431
--email hidden
passcode not visible
logged in users only

Tags, Category, Keywords and additional notes

orderings; theorem proving