L'unité d'enseignement ENSIN6U2
« Logique et calculabilité »

Appréhender l'intérêt des formalismes logiques pour l'informatique. Faire le lien entre une formule et un modèle. Représenter des connaissances de façon rigoureuse. Raisonner sur les connaissances.

• Calcul des propositions : vocabulaire, syntaxe et sémantique ; algorithme de Quine ; algorithme de Davis et Putnam ; méthodes basées sur la résolution, clauses de Horn ; théorème de compacité.
• Calcul des prédicats : vocabulaire, syntaxe et sémantique ; forme de Skolem et forme causale ; interprétation de Herbrand ; unification, méthode de résolution ; programmation logique, exemple de l'algorithme d'Euclide.
• Calculabilité : décidabilité et indécidabilité des formules ; notion de fonctions calculables et non-calculables ; thèse de Church, machine de Turing, lambda-calcul.

ENSIN2U2 Automates et circuits ; ENSIN3U2 Théorie des langages