[metis-users] KBO vs. LPO

[Jasmin Blanchette]

Hi Joe,

> Around ten(!) years ago I carried out some experiments with term
> orderings in Metis, specifically the "stickiness" of constraints on
> clauses resulting from KBO comparisons. I wrote them up in a Cambridge
> CL technical report:
> 
> http://www.gilith.com/research/papers/ordering.pdf
> 
> However, that reference was just for interest's sake. To answer your
> specific question, I would certainly consider adding different
> orderings to Metis. In Clause.sig the order is explicitly
> parameterized:
> 
> type parameters =
>     {ordering : KnuthBendixOrder.kbo,
>      orderLiterals : literalOrder,
>      orderTerms : bool}
> 
> If someone were to create a new module LexicographicPathOrder with the
> same signature as KnuthBendixOrder I would happily hook pull it in to
> the Metis sources and offer it as an option to Clause.parameters.

Since last week, I carried out some experiments with E and SPASS, both of which support both KBO and LPO, and I wasn't able to get the expected improvements on a large set of benchmarks -- although it helped a lot for a few examples I constructed. So I'm unlikely to pursue this further. But thanks anyway!

Cheers,

Jasmin