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,
René


> Am 16.05.2020 um 10:15 schrieb Jens-D. Doll <jens.doll at live.de>:
> 
> 
> 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.