Semaine du lundi 25 novembre 2024
Le programme de colles inclue à nouveau tout ce qui précède. On pourra notamment donner des exercices de déduction naturelle demandant de :
- démontrer des séquents, comme nous en avons pris l'habitude. L'équivalence entre "$\Gamma \models \varphi$" et "$\Gamma \vdash \varphi$ est démontrable" (correction et complétude du système de la déduction naturelle) a été vue, et il est attendu que les étudiants sachent l'utiliser pour deviner s'ils font fausse route lors de la construction d'un arbre de preuve.
- démontrer des règles, soit par une méthode directe (arbre de preuve partiel), soit par une méthode indirecte (par exemple, induction sur les arbres de preuve, comme pour la règle de l'affaiblissement)
- de manière plus générale, la méthode de démonstration par induction sur les arbres de preuve (pour démontrer que les séquents démontrables vérifient une propriété) a été vue et peut être demandée dans certains exercices.
- On peut donner quelques exercices de modélisation d'énoncés en formules du premier ordre, et les étudiants doivent être capables d'identifier chaque élément dans l'écriture d'une formule (symboles de prédicats, de fonctions, de variables, de constantes ; termes ; formules atomiques).
- Les opérations de renommages, substitutions, et la déduction naturelle étendue aux formules du premier ordre ne sont attendus dans les exercices, ces notions sont encore trop récentes et peu maîtrisées.
- Pour les plus avancés, on peut envisager de donner des exercices utilisant des systèmes de preuves autres que la déduction naturelle, et dont le but n'est pas nécessairement de construire des séquents, mais d'autres objets.
Les règles de la déduction naturelle devront toujours être données aux étudiants, mais il est attendu qu'ils sachent les utiliser. On peut également leur fournir d'autres règles (admises ou à redémontrer) ; les étudiants peuvent utiliser des séquents ou des règles classiques (tiers exclu, double négation, affaiblissement) qui n'ont pas été fournies, s'ils sont capables de les justifier.
