Free Boolean Algebra

 

Title: Free Boolean Algebra
Author: Brian Huffman
Submission date: 2010-03-29
Abstract: 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.
BibTeX:
@article{Free-Boolean-Algebra-AFP,
  author  = {Brian Huffman},
  title   = {Free Boolean Algebra},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2010,
  note    = {\url{http://isa-afp.org/entries/Free-Boolean-Algebra.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License