Disciplina Curricular

Lógica Funcional e Teoria da Demonstração LFTD

Diploma de Estudos Avançados em Segurança de Informação - DEASegInf2007

Contextos

Grupo: DEASegInf2007 > 3º Ciclo > Matemática > Lógica e Computação

Período:

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.