Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip 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: Nov 21 2024 at 12:39 UTC