[isabelle] 3 new AFP entries
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!
1. Lattice Properties by Viorel Preoteasa
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.
2. Algebra of Monotonic Boolean Transformers by Viorel Preoteasa
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).
3. Pseudo Hoops by George Georgescu, Laurentiu Leustean and Viorel Preoteasa
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and