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: Nov 21 2024 at 12:39 UTC