Boolean Expression Checkers

Tobias Nipkow

8 June 2014

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).
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.

Used by

Topics

Theories