Boolean Expression Checkers

Tobias Nipkow 🌐

June 8, 2014


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.


Theories of Boolean_Expression_Checkers