Disciplina Curricular
Lógica Funcional e Teoria da Demonstração LFTD
Mestrado Bolonha em Matemática e Aplicações e Computação - MMA 2006
Peso
7.5 (para cálculo da média)
Objectivos
Dominar a teoria matemática da lógica funcional, sua semântica operacional e sistemas de tipos, bem como a semântica e sistemas dedutivos das lógicas proposicionais clássica e intuicionista. Compreender a relação fundamental entre os sistemas de tipos para a lógica funcional e a teoria da demonstração clássica e intuicionista, e suas implicações.
Programa
Cálculo-lambda, teorias, coerência. Redução, formas normais, confluência, teorema de Church-Rosser. Determinadores de pontos-fixos, recursão, definabilidade e computabilidade, tese de Church-Markov-Turing, teorema de Kleene. Resultados de indecidibilidade, teorema de Rice. Lógica combinatória. Tipos simples, redução e normalização. Decidibilidade da tipificação de termos e da verificação de tipos, teorema de Hindley-Milner. O problema da habitação de tipos. Lógicas proposicionais clássica e intuicionista (LPC and LPI), álgebras de Boole e de Heyting, axiomatizações e tertium non datur, correcção e completude. Semântica de Kripke da LPI, propriedade do modelo finito, decidabilidade. Cálculo de sequentes, eliminação do corte, normalização, decidabilidade. A interpretação de Brouwer-Heyting-Kolmogorov da LPI. Habitação de tipos simples e o fragmento implicativo da LPI. O isomorfismo de Curry-Howard, coerência, normalização, decidibilidade da habitação de tipos. Tipos união e produto. Lógica clássica e operadores de controlo. Combinadores, relevância e linearidade. Lógica computacional, fórmulas-como-tipos e provas-como-programas, o lambda-cubo de Barendregt.
Metodologia de avaliação
Exame final.