Boolean Expression Checkers


Title: Boolean Expression Checkers
Author: Tobias Nipkow
Submission date: 2014-06-08
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).
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.
  author  = {Tobias Nipkow},
  title   = {Boolean Expression Checkers},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2014,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Used by: LTL_to_DRA