Manipulations de formules du calcul propositionnel

On considére l'ensemble des formules du calcul des propositions définies sur un ensemble de variables, les constantes vari et faux et les connecteurs de négation, conjonction, implication et équivalence.

On propose deux méthodes simples pour décider des tautologies propositionnelles.



1  Formes conjonctives et négatives normales

  1. Écrire une fonction de mise en forme négative normales. On utilise les lois de De Morgan, la traduction de l'implication en disjonction et négation, la traduction de l'équivalence en conjonction d'implication.
  2. Écrire une fonction qui traduit une forme négative normale en sa conjonctive normale. On utilise la distributivité. Le résultat sera une liste de listes d'atomes ou négation d'atomes. Un atome est une variable propositionnelle ou une constante. On prendra soin de ne pas avoir de duplication dans les disjonctions.
  3. En déduire une fonction qui décide si formule propositionnelle tautologie.

2  IF-expressions

On se donne le connecteur ternaire IF tel que : On appelle IF-expresssions les formules écrites avec ce connecteur.
  1. Écrire une fonction qui traduit une proposition en IF-expression.
  2. On dit qu'une IF-expression est en forme normale si elle est de la forme IF(X,e1,e2) oùX est une variable ou une constante et e1 et e2 sont en forme normales. Écrire une fonction qui met une IF-expression en forme normale.
  3. En déduire une fonction décide si une formule propositionnelle est une tautologie.
This document was translated from LATEX by HEVEA.