Email Gateway (Aug 18 2022 at 15:36): Email Gateway (Aug 18 2022 at 15:36):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
The Archive of Formal Proofs is now updated to Isabelle version 2009-2. As always, previous releases of entries remain available.
We're also pleased to announce one new entry:
Free Groups
by Joachim Breitner
Abstract:
Free Groups are, in a sense, the most generic kind of group. They are defined over a set of generators with no additional relations in between them. They play an important role in the definition of group presentations and in other fields. This theory provides the definition of Free Group as the set of fully canceled words in the generators. The universal property is proven, as well as some isomorphisms results about Free Groups.
as well as the release version of an entry previously available on in the development version of the Archive:
Regular Sets and Expressions
by Alexander Krauss and Tobias Nipkow
Abstract:
This is a library of constructions on regular expressions and languages. It provides the operations of concatenation, Kleene star and derivative on languages. Regular expressions and their meaning are defined. An executable equivalence checker for regular expressions is verified; it does not need automata but works directly on regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, concatenation and (reflexive) transitive closure is obtained.
2010 has so far been a good year for the Archive, it has now grown to 77 entries. Keep them coming in!
Cheers,
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC