08. Applications de la Logique

La logique au cœur de l’informatique

La logique mathématique n’est pas qu’une discipline abstraite — elle est le fondement théorique de l’informatique et trouve des applications concrètes dans de nombreux domaines.

Connexion historique

L’informatique est née de la logique:

• Turing (1936): La machine de Turing formalise la notion de calcul via des systèmes formels.
• Church (1936): Le lambda-calcul établit l’équivalence avec la calculabilité.
• Shannon (1937): L’algèbre booléenne décrit les circuits électroniques.

Aujourd’hui, la logique reste omniprésente: des portes logiques dans les processeurs aux systèmes de preuve automatique.

Circuits logiques

Portes logiques fondamentales

Les circuits numériques implémentent physiquement l’algèbre booléenne:

Universalité du NAND

Toute fonction booléenne peut être réalisée avec des portes NAND uniquement:

$$ \begin{aligned} \neg A &= A \uparrow A \ A \land B &= (A \uparrow B) \uparrow (A \uparrow B) \ A \lor B &= (A \uparrow A) \uparrow (B \uparrow B) \end{aligned} $$

Cette propriété est exploitée dans les circuits intégrés CMOS.

Circuits combinatoires

Un circuit combinatoire calcule une fonction booléenne pure: la sortie dépend uniquement des entrées actuelles.

Exemple: Additionneur 1 bit

Pour additionner deux bits $A$ et $B$ avec une retenue entrante $C_{in}$:

$$ \begin{aligned} Sum &= A \oplus B \oplus C_{in} \ C_{out} &= (A \land B) \lor (C_{in} \land (A \oplus B)) \end{aligned} $$

Circuits séquentiels

Les circuits séquentiels ont une mémoire (état). Leur comportement est modélisé par la logique temporelle.

Exemple: Une bascule RS (flip-flop) mémorise un bit:

• Set ($S = 1$): met la sortie à 1
• Reset ($R = 1$): met la sortie à 0

Bases de données et SQL

Le modèle relationnel

Le modèle relationnel (Codd, 1970) repose sur la logique du premier ordre:

• Une relation (table) est un ensemble de n-uplets.
• Les attributs sont les colonnes.
• Les requêtes sont des formules logiques.

SQL comme logique

Les clauses SQL correspondent à des opérations logiques:

Exemple de traduction

Requête: “Employés du département ‘Informatique’ gagnant plus de 50000”

SQL:

SELECT * FROM Employes
WHERE departement = 'Informatique' AND salaire > 50000

Logique: $$ {e \mid Employe(e) \land Dept(e) = \text{`Informatique’} \land Salaire(e) > 50000} $$

Calcul relationnel

Le calcul relationnel par tuples utilise directement la logique du premier ordre:

$$ {t \mid \varphi(t)} $$

où $\varphi$ est une formule avec $t$ comme variable libre.

Théorème (Codd): Le calcul relationnel et l’algèbre relationnelle ont le même pouvoir expressif.

Contraintes d’intégrité

Les contraintes sont des formules logiques que la base doit satisfaire:

Clé primaire: $$ \forall x , \forall y (Employe(x) \land Employe(y) \land Id(x) = Id(y) \rightarrow x = y) $$

Clé étrangère: $$ \forall e (Employe(e) \rightarrow \exists d (Departement(d) \land Dept(e) = Id(d))) $$

Vérification formelle

Motivation

Les bugs logiciels peuvent avoir des conséquences catastrophiques:

• Ariane 5 (1996): dépassement d’entier → explosion
• Therac-25 (1985-87): erreurs de concurrence → surdoses mortelles
• Intel FDIV (1994): erreur de division → rappel massif

La vérification formelle prouve mathématiquement qu’un système satisfait sa spécification.

Logique de Hoare

La logique de Hoare raisonne sur les programmes impératifs avec des triplets:

$$ {P} ; C ; {Q} $$

• $P$: précondition (ce qui est vrai avant)
• $C$: commande (le programme)
• $Q$: postcondition (ce qui est vrai après)

Exemple: $$ {x = n} ; x := x + 1 ; {x = n + 1} $$

Règles de Hoare

Affectation: $$ {P[e/x]} ; x := e ; {P} $$

Séquence: $$ \frac{{P} ; C_1 ; {Q} \quad {Q} ; C_2 ; {R}}{{P} ; C_1; C_2 ; {R}} $$

Conditionnelle: $$ \frac{{P \land B} ; C_1 ; {Q} \quad {P \land \neg B} ; C_2 ; {Q}}{{P} ; \text{if } B \text{ then } C_1 \text{ else } C_2 ; {Q}} $$

Model Checking

Le model checking vérifie automatiquement si un modèle fini satisfait une spécification en logique temporelle.

Logique temporelle CTL:

• $AG,\varphi$: “toujours $\varphi$”
• $EF,\varphi$: “potentiellement $\varphi$”
• $A[\varphi , U , \psi]$: “$\varphi$ jusqu’à $\psi$”

Exemple de spécification: $$ AG(requete \rightarrow AF,reponse) $$ “Toute requête reçoit éventuellement une réponse.”

Outils industriels

• SPIN: Vérification de protocoles
• NuSMV: Model checker symbolique
• Coq, Lean: Assistants de preuve
• Z3, CVC5: Solveurs SMT

Intelligence artificielle

Systèmes experts

Les premiers systèmes d’IA utilisaient la logique pour représenter les connaissances:

Base de connaissances: $$ \begin{aligned} &\forall x (Oiseau(x) \land \neg Anormal(x) \rightarrow Vole(x)) \ &Oiseau(tweety) \ &\neg Anormal(tweety) \end{aligned} $$

Inférence: $$ Vole(tweety) $$

Programmation logique (Prolog)

Prolog exécute des programmes comme des preuves logiques:

parent(tom, mary).
parent(mary, john).
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

Requête: ?- grandparent(tom, john). Réponse: true.

La sémantique de Prolog est basée sur la résolution et les clauses de Horn.

Logiques de description

Les logiques de description (DL) sont des fragments décidables de la logique du premier ordre, utilisés pour les ontologies:

Exemple (Web sémantique): $$ Etudiant \sqsubseteq Personne \sqcap \exists inscritA.Cours $$ “Un étudiant est une personne inscrite à au moins un cours.”

Satisfiabilité et SAT

Les solveurs SAT et SMT sont utilisés en IA pour:

• Planification automatique
• Raisonnement par contraintes
• Vérification de réseaux de neurones

Cryptographie et sécurité

Protocoles cryptographiques

La logique BAN (Burrows-Abadi-Needham) raisonne sur les protocoles de sécurité:

$$ P \text{ croit } Q \text{ a dit } X $$

“L’agent $P$ croit que l’agent $Q$ a énoncé $X$.”

Exemple: Authentification

Objectif: Après le protocole, $A$ croit que $B$ est authentique.

Formalisation: $$ A \text{ croit } B \text{ croit } K_{AB} $$

La logique permet de détecter des failles dans les protocoles (attaques man-in-the-middle, replay, etc.).

Théorie des types

Correspondance de Curry-Howard

La correspondance de Curry-Howard établit un isomorphisme:

Exemple: $$ (A \rightarrow B) \rightarrow (B \rightarrow C) \rightarrow (A \rightarrow C) $$

correspond au type:

compose : (A -> B) -> (B -> C) -> (A -> C)
compose f g = \x -> g (f x)

Assistants de preuve

Les assistants de preuve utilisent cette correspondance:

• Coq: Preuves formelles de théorèmes mathématiques
• Lean: Mathématiques formalisées (Mathlib)
• Agda: Théorie des types dépendants

Application: Le compilateur CompCert (C vérifié) a été prouvé correct en Coq.

Résumé des applications