loglangcoq.logique.introduction
- Objectif du document
- Que puis-je lire concernant ce cours?
- Qu'est-ce-que Coq?
- Pourquoi utiliser Coq dans ce cours?
loglangcoq.logique.lexique
- forall, exists, ∧, ∨, ⟶, etc
- Definition f:T := def.
- Fixpoint f (x1:t1) ... (xn:tn) : T := def. ou Function f (x1:t1) ... (xn:tn) : T := def.
- Lemma X: Y. ou Theorem X:Y.
- Notation "xxx" := (yyy)
- Commandes usuelles
- Inductive I : T := def
loglangcoq.logique.tables_de_verite
loglangcoq.logique.logique_generique
loglangcoq.logique.logique_propositionnelle
- Les formules propositionnelles (sans variables)
- Interprétation d'une formule (Sémantique)
- Preuves d'équivalences entre formules
- Réduction des connecteurs au sous-ensemble {⊤,¬,∨}
loglangcoq.logique.logique_propositionnelle_avec_variables
- Le formules propositionnelle avec variables propositionnelles
- Interprétation d'une formule (Sémantique)
- Conséquence, modèle etc
- Preuves d'équivalences entre formules
- Réduction des connecteurs au sous-ensemble {⊤,¬,∨}
- Preuve par réfutation (Utile pour la preuve par tableau plus loin).
- Preuve par la méthode des tableaux
loglangcoq.logique.logique_predicats
- Les formules
- Conséquence, modèle etc
- Preuves d'équivalences entre formules
- Preuve par réfutation (Utile pour la preuve par tableau plus loin).
- Preuve par la méthode des tableaux
loglangcoq.logique.logique_predicats_avec_quantificateurs
- Les formules
- Définition de l'interprétation d'une formule
- Conséquence, modèle etc
- Preuves d'équivalences entre formules
- Preuve par réfutation (Utile pour la preuve par tableau plus loin).
- Preuve par la méthode des tableaux
- Substitution de variable dans une formule
loglangcoq.logique.deduction_naturelle
- Préliminaires
- Déduction naturelle: Définition
- Propriétés remarquables de la déduction naturelles
- Correction de la déduction naturelle
- Préliminaires de la Preuve de complétude de la déduction naturelle
- Mesure sur une formule seule
- Définition de la mesure sur Γ⊢φ en vue de l'induction
- Quelques preuve de compatibilité de la mesure
- Lemmes auxiliaires sur consequance_set.
- Notion de formule atomique, litéral, etc
- Différentes disjonctions sur les termes
- Notion d'interprétation caractéristique d'un environnement
- Propriétés des environnements ne contenant que des litéraux
- Preuve de la complétude de la déduction naturelle
loglangcoq.logique.semantique
loglangcoq.logique.semantique_avec_routine
loglangcoq.logique.semantique_avec_procedure
This page has been generated by coqdoc