### 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

- Computer science/Algorithms
- Logic/General logic/Mechanization of proofs

### Session Boolean_Expression_Checkers

- Boolean_Expression_Checkers
- Boolean_Expression_Checkers_AList_Mapping
- Boolean_Expression_Example

### Used by

- Linear Temporal Logic
- Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata

## Cite

×

Boolean_Expression_Checkers-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Jun 8, 2014 : Isabelle2013-2