Boolean Expression Checkers

Tobias Nipkow 🌐

June 8, 2014

Abstract

This entry provides executable checkers for the following properties of boolean expressions: satisfiability, tautology and equivalence. Internally, the checkers operate on binary decision trees and are reasonably efficient (for purely functional algorithms).
BSD License

Change history

[2015-09-23] Salomon Sickert added an interface that does not require the usage of the Boolean formula datatype. Furthermore the general Mapping type is used instead of an association list.

Topics

Theories of Boolean_Expression_Checkers

Used by

Cite

× 
@article{Boolean_Expression_Checkers-AFP,
  author  = {Tobias Nipkow},
  title   = {Boolean Expression Checkers},
  journal = {Archive of Formal Proofs},
  month   = June,
  year    = 2014,
  note    = {\url{https://isa-afp.org/entries/Boolean_Expression_Checkers.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest