##
BDDC v2 |

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.

- Description
- Lexical aspects
- Commands
- Logical expressions
- Appendix
- Examples
- References

This document was translated from L^{A}T_{E}X byH^{E}V^{E}A.