# 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.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: LTL, LTL_to_DRA