Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 23 2022 at 09:09):

From: "Jens-D. Doll" <jens.doll@live.de>
Does this (order) formalization define an algorithm for term
reduction(s)?
Jens

Last updated: Feb 15 2026 at 05:19 UTC