Derniers contenus

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.

Pour cette semaine, le programme de colles concerne tout ce qui a été vu précédemment, et inclut notamment :

Dans le chapitre d'algorithmique des graphes :

- la connaissance du problème de couplage maximal dans un graphe biparti

- la connaissance du lemme de Berge

- l'algorithme par recherche de chemin augmentant qui en découle ; il faut en connaître au moins le grand principe : on recherche un chemin augmentant depuis chaque sommet de $S_1$, on calcule le nouveau couplage par différence symétrique, et on recommence ; chaque recherche de chemin augmentant se fait par parcours en profondeur depuis le sommet d'origine.

Dans le chapitre de déduction naturelle :

- construction d'arbres de preuves simples à partir des règles de la déduction naturelle ; les règles ne sont pas à connaître par coeur, et devront être fournies, mais il faut savoir les utiliser

- l'équivalence entre "$\Gamma \models \varphi$" et "$\Gamma \vdash \varphi$ est démontrable" n'a pas encore été prouvée, mais est à connaître pour s'aider dans la construction des arbres, afin de juger si un séquent intermédiaire peut être démontré ou non

- la notion de "démontrer une règle" n'a pas encore été vue, mais peut être utilisée dans un exercice si elle est réexpliquée. En particulier, la règle de l'affaiblissement n'a pas encore été vue.

- aucune implémentation n'est attendue autour de la construction d'arbres de preuves