Disciplina Curricular
Lógica Computacional LCom
Mestrado Bolonha em Matemática e Aplicações e Computação - MMA 2006
Peso
7.5 (para cálculo da média)
Objectivos
Dominar os fundamentos matemáticos dos sistemas de demonstração automática, do cálculo-lambda tipado e da teoria da demonstração. Representar lógicas, construir e verificar demonstrações e extrair delas programas funcionais, usando o moderno sistema de demonstração automática Isabelle, com ênfase em aplicações à engenharia da programação e à inteligência artificial.
Programa
Fundamentos. Teoria da demonstração, cálculo-lambda tipado, isomorfismo de Curry-Howard e o lambda-cubo de Barendregt. Lógica de primeira-ordem, semântica e sistema dedutivo, semi-decidibilidade. Tipos dependentes, julgamentos, o sistema de tipos lambda-P. Lógica de segunda-ordem, semântica e sistema dedutivo, indecidibilidade. Tipos polimórficos, o sistema de tipos lambda-2. Lógica de ordem-superior, semântica e sistema dedutivo, indecidibilidade. Sistemas de tipos puros e suas propriedades. Aplicações. Introdução ao sistema de demonstração automática Isabelle. Representação de lógicas, dedução natural, cálculos de sequentes e representações semânticas. Construção e verificação de demonstrações. Representação de lógicas modais e de sistemas dedutivos etiquetados. Lógica de primeira-ordem multi-género, teoria de conjuntos de Zermelo-Fraenkel e a extensão FOL/ZF do sistema Isabelle. Lógica de ordem-superior e a extensão HOL do sistema Isabelle. Extracção de programas funcionais.
Metodologia de avaliação
Exame final (ou 2 testes) (60%), projecto (40%).