918 - Systèmes formels de preuve en logique du premier ordre. Exemples.2021

Rapport du jury 2019

Le jury attend du candidat qu’il présente au moins la déduction naturelle ou un calcul de séquents et qu’il soit capable de développer des preuves dans ce système sur des exemples classiques simples. $\\$ La présentation des liens entre syntaxe et sémantique, en développant en particulier les questions de correction et complétude, et de l’apport des systèmes de preuves pour l’automatisation des preuves est également attendue. Le jury apprécie naturellement si des candidats présentent des notions plus élaborées comme la stratégie d’élimination des coupures mais est bien conscient que la maîtrise de leurs subtilités va au-delà du programme.