Re: [isabelle] New in the AFP: A Formalization of Knuth–Bendix

Hi Jens,

well definitely such a generator is not part of the AFP-entry.
Note that for KBO, it necessarily must return some infinite list or sequence.

E.g., consider a signature with symbol 0(unary), 1(constant), 2(constant) which all have their own weight,
and where 1 is highest in precedence.

Then in KBO we have

2 > 1
2 > 0(1)
2 > 0(0(1))
2 > …

so for reducing 2, you have to produce the infinite list 1, 0(1), 0(0(1)), …


> Am 18.05.2020 um 09:51 schrieb Jens-D. Doll <jens.doll at>:
> It would be useful to have a generator. If we also have a term order and terms are enumerable, the first approach for algorithms could be:
>  a) enumerate all pairs (term,term) and
>  b) decide if they are reducible
> That could lead to a generalized TRS.
> Jens

Attachment: signature.asc
Description: Message signed with OpenPGP

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.