CS 2800: Lógica e Computação Primavera 2019

Este curso fornece uma introdução à lógica formal e suas conexões profundas à computação. A lógica é apresentada de uma perspectiva acomputacional usando o sistema de prova ACL2 Sedantheorem. O objetivo do curso é introduzir métodos fundamentais e fundacionais para modelagem, desenho e raciocínio sobre computação, incluindo lógica proposicional, recursividade, indução, raciocínio equacional, análise de terminação, reescrita e várias técnicas de prova. Mostramos como usar a lógica para formalizar a sintaxe e semântica do núcleo da linguagem ACL2s, uma linguagem simples baseada em LISP com contratos. Usamos então a linguagem ACL2s para raciocinar formalmente sobre programas, para modelar sistemas em vários níveis de abstração, para projetar e especificar interfaces entre sistemas e para raciocinar sobre tais sistemas compostos. Nós também examinamos procedimentos de decisão para fragmentos de lógica de ordem de partida e como tais procedimentos de decisão podem ser usados para analisar modelos de sistemas.

Os pré-requisitos são uma familiaridade básica com programação funcional (CS 2500) e estruturas discretas (CS 1800). Se você não tem esse histórico, você precisa da permissão do seu instrutor.

Os alunos que estão frequentando a classe são obrigados a verificar Piazza para anúncios diariamente.