Free Boolean Algebra

Brian Huffman 🌐

March 29, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session Free-Boolean-Algebra

Cite

× 
@article{Free-Boolean-Algebra-AFP,
  author  = {Brian Huffman},
  title   = {Free Boolean Algebra},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2010},
  note    = {\url{https://isa-afp.org/entries/Free-Boolean-Algebra.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: