Binary Decision Diagrams

Il progetto descrive i principali concetti relativi ai Binary Decision Diagrams(BDD), una compatta struttura per la rappresentazione di funzioni booleane. Viene spiegato cosa sono, le caratteristiche e proprietà che presentano, come crearli, le principali operazioni possibili con essi e il loro impiego nel model checking.
Inoltre viene fornita un'implementazione in Prolog dell'algoritmo di creazione proposto, in modo da poter testare le caratteristiche discusse. L'algoritmo fornisce la possibilità creare un BDD partendo da una formula booleana contenente gli operatori logici negazione, implicazione, or e and.