AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS   Info

AG Audience

English

60 Minutes

Saarbrücken

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

orderings; theorem proving