Logique & Démonstration

Introduction à la logique propositionnelle

Une logique pour exprimer des propositions

Une proposition

C’est une phrase, une formule, une affirmation, qui peut être vraie ou fausse

• ✅ “Il fait beau”
• ✅ “Si je suis un génie ou si je travaille bien, alors je n’irai pas au rattrapage”
• ✅“42+0=42”
• ✅ “\(p\to (p\land (r\lor \lnot q))\)”
• ✅“42-0=58”
• ✅“Le serveur est ouvert aux inscriptions”

• ❌ “Allons à la pêche !”
• ❌ “42 + 12”
• ❌ “salade, tomates, oignons”
• ❌ “Le serveur”
• ❌ “Le serveur est-il ouvert aux inscriptions ?”

Vérifier un programme

1) Exprimer la propriété voulue

(* Exclusion : banni ou en queue de matchmaking *)
Theorem expulse_si_banni : forall j : joueur,
  banni j \/ en_attente j -> peut_rejoindre_raid j = false.

(* Condition nécessaire *)
Theorem niveau_necessaire : forall j : joueur,
  peut_rejoindre_raid j = true -> niveau_suffisant j.