Outils Logiques pour l'Informatique

Ces notes sont une introduction `à la logique mathématique et aux techniques de d´éduction automatique dans le cadre du calcul propositionnel classique avec des applications à la résolution de problèmes combinatoires et `à la modélisation et analyse de systèmes informatiques.

La logique est à l'origine une réflexion sur le discours (logos) et sur sa cohérence. En particulier, la logique mathématique s'intéresse à l'organisation et à la cohérence du discours mathématique et donc aux notions de validité et de preuve. Dans le calcul propositionnel classique, on dispose d'un certain nombre de propositions qui peuvent être vraies ou fausses et d'un certain nombre d'opérateurs qui permettent de combiner ces propositions.

Remarquons que les mesures de complexité que nous avons évoquées pour les circuits logiques ont une interprétation immédiate en termes de circuits combinatoires. Le nombre de nÅ?uds du circuit booléen correspond au nombre de portes logiques, câ??est-à-dire au nombre de transistors n´nécessaires à la mise en Å?uvre du circuit. Couplée avec la topologie des inter- connexions, cette mesure détermine l'espace occupé par le circuit. La longueur du chemin le plus long correspond au temps qu'il faut attendre entre une variation du signal en entrée et la stabilisation du signal en sortie.

La notion de circuit booléen fait abstraction de la notion de temps (le calcul du résultat est instantané) et dans une certaine mesure de distance (on compte le nombre de portes mais on ne compte pas la longueur des interconnexions) et il permet de simplifier grandement la conception d'un circuit combinatoire. Dans la suite nous allons considérer dans un certain détail la conception d'un additionneur.

Il est trivial de construire des systèmes corrects ou complets mais il est beaucoup plus d´délicat de construire des systèmes corrects et complets. On va examiner un système correct et complet proposé par Gerhard Gentzen en 1930. Une idée générale est d'´écrire des règles d'inférence qui permettent de redire la 'complexité structurale (ou logique)' des formules jusqu'`a une situation qui peut être traitée directement par un axiome.