Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Free Boolean Algebra by Brian H...

Email Gateway (Aug 18 2022 at 15:00):

From: Tobias Nipkow <nipkow@in.tum.de>
http://afp.sourceforge.net/entries/Free-Boolean-Algebra.shtml

This theory defines a type constructor representing the free Boolean
algebra over a set of generators. Values of type (?)formula represent
propositional formulas with uninterpreted variables from type ?, ordered
by implication. In addition to all the standard Boolean algebra
operations, the library also provides a function for building
homomorphisms to any other Boolean algebra type.

Thanks Brian!
Tobias

Last updated: Apr 20 2024 at 01:05 UTC