Boolean Expression Checkers

Tobias Nipkow 🌐

June 8, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


September 23, 2015
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.


Session Boolean_Expression_Checkers