TP 1 : Logique propositionnelle




Ce document est disponible à l'URL http://www.liafa.jussieu.fr/~sighirea/logver/tp_01.html

Ce TP sera effectué sur la machine ``cunillet''.

Dans la traduction en HTML des symboles mathématiques, les correspondances suivantes ont été utilisées :

Symbole Sémantique
Î appartient à
Ï n'appartient pas à
 .  et logique
 +  ou logique
 xor  ou exclusif logique

1   Formes normales pour les formules booléennes

Nous utiliserons le logiciel bddc (BDD Calculator) inclus dans la distribution des logiciels pour le langage Lustre.
Appel :
~sighirea/LogVer/lustre/bin/bddc
Aide :
tapez help à l'invité de commande
Syntaxe des commandes :
tapez syntax à l'invité de commande
Exercice 0 :
Vérifiez les formes normales disjonctives et Reed-Muller obtenues en TD à l'exercice 3. Exemples : 
> - (p * - (q + s))
...
> reed - (p * - (q + s))
Exercice 1 :
Obtenez la forme Reed-Muller pour toutes les expressions booléennes vues en TD.

2   Décomposition de Shannon

Toujours avec l'outil bddc.

Exercice 2 :
En utilisant les commandes root, left etright, déterminez la décomposition de Shannon pour les expressions vues en TD.

3   Diagrammes de décision binaire

Nous utilisons pour cela le logiciel boole du package de BDD CMU.
Appel :
~sighirea/LogVer/cmubdd/bin/sun4/boole -i
Syntaxe des commandes :
voir ~sighirea/LogVer/cmubdd/boole/README
Exercice 3 :
En utilisant la commande print, obtenez les BDD pour les expressions booléennes vues en TD.

Exercice 4 :
En utilisant la commande size, observez la tailles des BDD obtenus. Expliquez les résultats.
Ce document a été traduit de LATEX par HEVEA.