CS 2800: Lógica y Computación Primavera 2019

Este curso proporciona una introducción a la lógica formal y sus profundas conexiones con la computación. La lógica se presenta desde una perspectiva computacional utilizando el sistema de demostración de teoremas ACL2 Sedan. El objetivo del curso es introducir métodos fundamentales para modelar, diseñar y razonar sobre la computación, incluyendo la lógica proposicional, la recursividad, la inducción, el razonamiento ecuacional, el análisis de terminación, la reescritura y varias técnicas de prueba. Mostramos cómo utilizar la lógica para formalizar la sintaxis y la semántica del núcleo del lenguaje ACL2s, un lenguaje sencillo basado en LISP con contratos. A continuación, utilizamos el lenguaje ACL2s para razonar formalmente sobre los programas, para modelar sistemas en varios niveles de abstracción, para diseñar y especificar interfaces entre sistemas y para razonar sobre dichos sistemas compuestos. También examinamos los procedimientos de decisión para fragmentos de lógica de primer orden y cómo dichos procedimientos de decisión pueden utilizarse para analizar modelos de sistemas.

Los requisitos previos son una familiaridad básica con la programación funcional (CS 2500) y las estructuras discretas (CS 1800). Si usted no tiene este fondo, necesita el permiso de su instructor.

Los estudiantes que toman la clase están obligados a comprobar Piazza para los anuncios diarios.