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

I interpret that you want to have an algorithm that given two terms s and t, you want to decide whether s >KBO t holds,
where also all parameters of KBO are provided.

Yes, such an algorithm is available. In fact, “kbo” in Isabelle is directly defined as an executable function
of type “term -> term -> (bool,bool)” where the two Booleans indicate whether the terms are in >KBO or in >=KBO relation.

Best regards,

> Am 16.05.2020 um 10:15 schrieb Jens-D. Doll <jens.doll at>:
> Does this (order) formalization define an algorithm for term reduction(s)?
> Jens

Attachment: signature.asc
Description: Message signed with OpenPGP

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