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.

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

License

BSD License

History

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.

Topics

Session Boolean_Expression_Checkers

Used by

Cite

× 
@article{Boolean_Expression_Checkers-AFP,
  author  = {Tobias Nipkow},
  title   = {Boolean Expression Checkers},
  journal = {Archive of Formal Proofs},
  month   = {June},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Boolean_Expression_Checkers.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: