A Knuth-Bendix-Like Ordering for Orienting Combinator Equations (Technical Report)
EasyChair Preprint 3191
24 pages•Date: April 18, 2020Abstract
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