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.
BibTeX:
@article{Boolean_Expression_Checkers-AFP,
  author  = {Tobias Nipkow},
  title   = {Boolean Expression Checkers},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Boolean_Expression_Checkers.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Used by: LTL_to_DRA