BDDC v2
A basic bdd-based logical calculator

Pascal RAYMOND

November 24, 2008, (rev. September 28, 2015)

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.