Email Gateway (Aug 18 2022 at 15:31): Email Gateway (Aug 18 2022 at 15:31):From: Tobias Nipkow <nipkow@in.tum.de>
There are two nicely modular new entries by Christian Sternagel and René
Thiemann from Innsbruck:
Abstract Rewriting
We present an Isabelle formalization of abstract rewriting (see, e.g.,
the book by Baader and Nipkow). First, we define standard relations like
joinability, meetability, conversion, etc. Then, we formalize important
properties of abstract rewrite systems, e.g., confluence and strong
normalization. Our main concern is on strong normalization, since this
formalization is the basis of CeTA (which is mainly about strong
normalization of term rewrite systems). Hence lemmas involving strong
normalization constitute by far the biggest part of this theory. One of
those is Newman's lemma.
http://afp.sourceforge.net/entries/Abstract-Rewriting.shtml
Executable Matrix Operations on Matrices of Arbitrary Dimensions
We provide the operations of matrix addition, multiplication,
transposition, and matrix comparisons as executable functions over
ordered semirings. Moreover, it is proven that strongly normalizing
(monotone) orders can be lifted to strongly normalizing (monotone)
orders over matrices. We further show that the standard semirings over
the naturals, integers, and rationals, as well as the arctic semirings
satisfy the axioms that are required by our matrix theory. Our
formalization is part of the CeTA system which contains several
termination techniques. The provided theories have been essential to
formalize matrix-interpretations and arctic interpretations.
http://afp.sourceforge.net/entries/Matrix.shtml
Enjoy!
Last updated: Nov 21 2024 at 12:39 UTC