Email Gateway (Aug 18 2022 at 18:26): Email Gateway (Aug 18 2022 at 18:26):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
We are please to announce the availability of 3 new AFP entries at [http://afp.sf.net].
This brings the number of AFP entries over 100!
This formalization introduces and collects some algebraic structures based on lattices and complete lattices for use in other developments. The structures introduced are complete distributive lattices, modular and distributive lattices, as well as lattice ordered groups. In addition to the results proved for the new lattices, this formalization also introduces theorems about latices and distributive lattices in general.
Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We formalize here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of this algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself).
Pseudo-hoops are algebraic structures introduced by B. Bosbach under the name of complementary semigroups. In this formalization we prove some properties of pseudo-hoops and we define the basic concepts of filter and normal filter. The lattice of normal filters is isomorphic with the lattice of congruences of a pseudo-hoop. We also study some important classes of pseudo-hoops. Bounded Wajsberg pseudo-hoops are equivalent to pseudo-Wajsberg algebras and bounded basic pseudo-hoops are equiv- alent to pseudo-BL algebras. Some examples of pseudo-hoops are given in the last section of the formalization.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 18:27):From: Victor Porton <porton@narod.ru>
What's about formalizing in Isabelle the concept of dual lattices using locales? ( I haven’t found the word :"dual" in Lattice_Infix.)
I noted previously that to do this one need the ability to define locales inside locales, and Isabelle misses this.
Will this every be done?
Email Gateway (Aug 18 2022 at 18:28):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Victor,
The class lattice_infix is just a wrapper around the lattice class from
the standard Isabelle library. I added this class just as a work around
for some feature that I could not get directly from the library.
However lattice_infix will become obsolete with the next release of
Isabelle which adds support for the features built in lattice_infix.
Best regards,
Viorel
Last updated: Apr 18 2024 at 16:19 UTC