CS 2800 : Logique et calcul Printemps 2019

Ce cours fournit une introduction à la logique formelle et à ses liens profonds avec l’informatique. La logique est présentée d’un point de vue informatique en utilisant le système de preuves Sedantheorem ACL2. L’objectif du cours est d’introduire des méthodes fondamentales pour modéliser, concevoir et raisonner sur l’informatique, y compris la logique propositionnelle, la récursion, l’induction, le raisonnement équationnel, l’analyse de la terminaison, la réécriture et diverses techniques de preuve. Nous montrons comment utiliser la logique pour formaliser la syntaxe et la sémantique du noyau du langage ACL2s, un langage simple basé sur LISP avec des contrats. Nous utilisons ensuite le langage ACL2s pour raisonner formellement sur des programmes, pour modéliser des systèmes à différents niveaux d’abstraction, pour concevoir et spécifier des interfaces entre systèmes et pour raisonner sur de tels systèmes composés. Nous examinons également les procédures de décision pour les fragments de la logique du premier ordre et comment ces procédures de décision peuvent être utilisées pour analyser les modèles de systèmes.

Les conditions préalables sont une familiarité de base avec la programmation fonctionnelle (CS 2500) et les structures discrètes (CS 1800). Si vous n’avez pas ces connaissances, vous avez besoin de la permission de votre instructeur.

Les étudiants qui suivent le cours sont tenus de vérifier Piazza pour les annonces quotidiennes.