Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 23 2022 at 09:10):

From: "Jens-D. Doll" <jens.doll@live.de>
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

Last updated: Apr 18 2024 at 20:16 UTC