Disciplina Curricular

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

Diploma de Estudos Avançados em Matemática - DEAMat2006

Contextos

Grupo: DEAMat2006 > 3º Ciclo > 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.

Metodologia de avaliação

Exame final.

Disciplinas Execução

2016/2017 - 2ºSemestre

2015/2016 - 2º Semestre

2014/2015 - 2º Semestre

2013/2014 - 2 Semestre

2012/2013 - 2 Semestre

2011/2012 - 2 Semestre

2010/2011 - 2 Semestre

2009/2010 - 2 Semestre

2008/2009 - 2 Semestre

2007/2008 - 2 Semestre