Higher-Order Critical Pairs

Abstract. We extend the termination proof methods based on reduction orderings to higher-order rewriting systems `a la Nipkow using higher-order pattern matching for firing rules, and accommodate for any use of eta, as a reduction, as an expansion or as an equation. As a main novelty, we provide with a mechanism for transforming any reduction ordering including beta-reduction, such as the higher-order recursive path ordering, into a reduction ordering for proving termination of rewriting `a la Nipkow. Non-trivial examples are carried out.

• Type: Conference
• Year: 1991
• Where: LICS
• Authors: Tobias Nipkow
• Keywords: Automated Reasoning, La Nipkow, LICS 1991, Reduction Ordering, Termination Proof Methods