A Knuth-Bendix-Like Ordering for Orienting Combinator Equations (Technical Report)

EasyChair Preprint 3191

Abstract

We extend the graceful higher-order basic Knuth-Bendix order (KBO)
of Becker et al. to an ordering that orients combinator equations left-to-right. The
resultant ordering is highly suited to parameterising the first-order superposition
calculus when dealing with the theory of higher-order logic, as it prevents infer-
ences between the combinator axioms. We prove a number of desirable proper-
ties about the ordering including it having the subterm property for ground terms,
being transitive and being well-founded. The ordering fails to be a reduction or-
dering as it lacks compatibility with certain contexts. We provide an intuition of
why this need not be an obstacle when using it to parameterise superposition.

Keyphrases: Knuth-Bendix, combinator, higher-order, rewriting, superposition, term ordering

@booklet{EasyChair:3191,
  author    = {Ahmed Bhayat and Giles Reger},
  title     = {A Knuth-Bendix-Like Ordering for Orienting Combinator Equations (Technical Report)},
  howpublished = {EasyChair Preprint 3191},
  year      = {EasyChair, 2020}}