A basic bdd-based logical calculator


November 24, 2008, (rev. September 30, 2022)

BDDC is a tool for manipulating logical formula. It is based on a Binary Decision Diagram library, that means that each formula is internally tranformed into a canonical form. In particular, if the formula (resp its negation) is a tautologie, BDDC will transform it into the "always true formula" (resp. the "always false formula").

All classical operators are provided. Moreover the tool provides a "functional-like" language that allows the user to define his (her) own logical operators.

This document was translated from LATEX by HEVEA.