Simplifier not (a and not b) à l'aide des lois de De Morgan

La simplification. De Morgan échange and et or en passant la négation à l'intérieur :

$$\text{not}(a\text{and}\text{not}b)=(\text{not}a)\text{or}\text{not}(\text{not}b)=(\text{not}a)\text{or}b.$$

On reconnaît l'implication $a\Rightarrow b$ : « si $a$ alors $b$ » est faux dans le seul cas $a$ vrai et $b$ faux.

La vérification automatique.

def equivalentes(f, g):
    """Vrai si f et g ont la meme table de verite (2 variables).

    Precondition : f et g prennent deux arguments booleens. On teste
    les 4 = 2**2 lignes, ce qui est une PREUVE : la table est finie.
    """
    return all(f(a, b) == g(a, b)
               for a in (False, True) for b in (False, True))

>>> equivalentes(lambda a, b: not (a and not b),
...              lambda a, b: (not a) or b)
True

Ce qui rend la logique confortable. Sur $n$ variables il y a $2^n$ lignes : un nombre fini. Un test exhaustif n'est donc pas un échantillonnage, c'est une démonstration complète. C'est un luxe rarissime en informatique — on ne peut pas tester une fonction sur tous les entiers.

Prolongement : le luxe a un prix. À $n=30$ variables, $2^{30}$ dépasse le milliard de lignes : la démonstration exhaustive devient impraticable. C'est le problème SAT, l'un des plus célèbres de l'informatique théorique.