This document is also available in PDF format.
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.