Logique & Démonstration

Introduction

Logique

Vérité des formules, vérité des raisonnements

• S’il fait nuit, les monstres attaquent
• Il fait nuit
• Les monstres attaquent

• S’il fait nuit, les monstres attaquent
• Il ne fait pas nuit
• Les monstres n’attaquent pas

• S’il fait nuit, les monstres attaquent
• Les monstres n’attaquent pas
• Il ne fait pas nuit

• S’il fait nuit, les monstres attaquent
• Les monstres n’attaquent pas
• Il ne fait pas nuit mais soit les monstres attaquent soit il fait jour, et si les monstres n’attaquent pas alors soit il fait jour, soit il fait nuit mais il n’y a plus de monstres; mais s’il y a des monstres alors ils peuvent attaquer même s’il fait jour, ou bien ils ne peuvent pas attaquer parce qu’ils explosent.

def is_server_available(server_online, whitelist_enabled,
                                   player_is_whitelisted, ban_active,
                                   max_players, current_players,
                                   maintenance, op_override):
    return (
        (server_online and not maintenance and not ban_active
         and (not whitelist_enabled or player_is_whitelisted)
         and (current_players < max_players or op_override))
        or (op_override and server_online and not ban_active)
        or (not server_online and not maintenance
            and op_override and not ban_active)
    ) and not (maintenance and not op_override)

Démonstrations…

• Pourquoi ?
• Quoi ?
• Comment ?

Pourquoi on veut démontrer ?

📐 En mathématiques

• Tous les résultats reposent sur des démonstrations
• La preuve est parfois plus importante que le résultat lui-même

💻 En informatique

• Application des maths :
  On utilise les mathématiques pour raisonner sur les programmes et les systèmes.
• Objectif : Prouver l’absence de bugs dans les programmes pour garantir leur fiabilité.

Deux grandes approches

🧪 Tester

test

✅ Prouver

preuve

Tester

Avantages

• Rapide
• Souvent plus facile

⚠ Inconvénients

• pas toujours scientifique
• Ne couvre pas tous les bugs

Program testing can be used to show the presence of bugs, but never to show their absence

Dijkstra

Preuve formelle

Avantages

• Garanties scientifiques
• Repose sur les maths

Inconvénients

• Repose sur les maths

Exemple : admin d’un serveur

On veut vérifier que les accès sont cohérents avec les règles du serveur :

• Connexion impossible si
  • ban
  • compte non créé
  • psswd incorrect
  • plus de 50 joueurs déjà connectés

• Ban si
  • plus de 10 messages en 30 secondes
  • partage de comptes
  • utilisation de mods interdits

On teste

# Test unitaire pour vérifier le ban de spam
def test_ban_spam():
    joueur = Joueur("Sarah")
    for _ in range(11):
        joueur.envoyer_message("Spam!") 

    if(joueur.est_banni()):
        print("test ban 1 OK")
    else:
        print("test ban 1 échec")

On prouve

Theorem ban_rules :
    (msg_30_sec > 10 \/ account_nb_user > 1 \/ forbidden_mod) -> ban.
Proof.
    …
Qed.

Theorem connexion_rules :
    (ban \/ wrong_psswd \/ nb_players>=50 \/ unregistered) -> ~connect.
Proof.
    …
Qed.

Un logicien est il encore utile en 2026 ?

L’IA peut-elle éviter d’avoir à faire ce travail pénible ?

Une question de spécification

flowchart LR
    A["Déterminer ce qui doit </br> être vérifié"]
    B["Écrire les théorèmes </br> à prouver"]
    C["**Écrire les preuves**"]
    D("Certifier les preuves </br> avec un outil fiable")

    A --> B
    B --> C
    C --> D

Où est-ce que ça pourrait mal se passer ?

Theorem all_numbers_are_even : 
    forall (n:nat), exists (m:nat), m>=0 /\ m*2=n
        \/ 2+2=4.
    
Proof.
    intro n. exists 42. right. simpl. reflexivity.
Qed.

Un outil logiciel pour la preuve : Rocq

`

Dans la suite de ce cours

• Maîtriser des méthodes de démonstration formelle
  • Tables de vérité
  • Déduction naturelle
  • Interprétation des formules
  • Rocq
• Les appliquer à différentes logiques
  • Logique propositionnelle
  • Logique du premier ordre (avec variables et prédicats)
  • Arithmétique