Lógica Avançada e Aplicações

Código:

CC4086

Sigla:

CC4086

Nível:

400

Áreas Científicas
Classificação	Área Científica
OFICIAL	Ciência de Computadores

Ocorrência: 2024/2025 - 2S

Ativa?	Sim
Unidade Responsável:	Departamento de Ciência de Computadores
Curso/CE Responsável:	Mestrado em Ciência de Computadores

Ciclos de Estudo/Cursos

Sigla	Nº de Estudantes	Plano de Estudos	Anos Curriculares	Créditos UCN	Créditos ECTS	Horas de Contacto	Horas Totais
M:CC	5	PE a partir do ano letivo de 2014	1	-	6	42	162

Língua de trabalho

Português - Suitable for English-speaking students

Objetivos

Resultados de aprendizagem e competências

No final da disciplina, pretende-se que o aluno:
- perceba a importância da utilização da lógica e dos sistemas formais na resolução de problemas concretos;
- seja capaz de relacionar teoria de prova com programação em diversos paradigmas (com enfase para o funcional e lógico);
- seja capaz de utilizar um sistema automático ou interativo de demonstração;
- perceba a interpretação algorítmica da lógica intuicionista e os princípios de extração de programas a partir de provas.

Modo de trabalho

Presencial

Programa

Bibliografia Obrigatória

Morten Heine Sørensen and Pawel Urzyczyn; Lectures on the Curry-Howard Isomorphism, Elsevier Science, 2006. ISBN: 978-0444520777
Jean Goubault-Larrecq; Proof theory and automated deduction. ISBN: 978-0-7923-4593-0
Yves Bertot; Interactive theorem proving and program development. ISBN: 9783540208549 hbk

Bibliografia Complementar

Samuel Mimram; Program = Proof, 2020. ISBN: 979-8615591839
Pedro Miguel Pereira Soares da Cunha; Homotopy type theory
Michael Huth; Logic in Computer Science. ISBN: 0-521-54310-X

Métodos de ensino e atividades de aprendizagem

Aulas teóricas-práticas com exposição de matéria e resolução de problemas.

Software

Coq Proof Assistant

Palavras Chave

Ciências Físicas > Ciência de computadores
Ciências Físicas > Matemática > Lógica matemática

Tipo de avaliação

Avaliação distribuída sem exame final

Componentes de Avaliação

Designação	Peso (%)
Teste	100,00
Total:	100,00

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	120,00
Frequência das aulas	42,00
Total:	162,00

Obtenção de frequência

Sem critérios de frequência.

Fórmula de cálculo da classificação final