Disciplina Curricular
Lógica e Verificação de Modelos LVM
Mestrado Bolonha em Matemática e Aplicações e Computação - MMAC 2021
Contextos
Grupo: MMAC 2021 > 2º Ciclo > Área Principal > Áreas de Especialização > Área de Especialização em Lógica e Computação > Área Científica de Lógica e Computação > Obrigatórias
Período:
Grupo: MMAC 2021 > 2º Ciclo > Área Principal > Áreas de Especialização > Área de Especialização em Lógica e Computação > Área Científica de Lógica e Computação > Obrigatórias
Período:
Peso
9.0 (para cálculo da média)
Objectivos
Conhecer programação em lógica, aplicar lógica à verificação de software e hardware.
Programa
Lógica proposicional. Diagramas de decisão binária. Lógica temporal ramificada (CTL). Verificação de modelos. Justiça forte e fraca. Caracterização dos operadores CTL por ponto fixo. Lógica temporal linear e cálculo mu proposicional. Verificação de sistemas concorrentes e distribuídos. Introdução à programação lógica. Lógica clausal, modelos de Herbrand. Algoritmo de unificação. Teorema do ponto fixo de Tarski. Programação funcional. Cálculo lambda. Topologia de Scott. Confluência e Combinadores. Cálculo lambda tipado e lógica de ordem superior. Prova automática de teoremas.
Metodologia de avaliação
Exame 50% e Projeto 50% (avaliado oralmente).
Componente de Competências Transversais
A UC permite o desenvolvimento de competências transversais em Pensamento Crítico, Criatividade e Estratégias de Resoluções de Problemas, nas aulas, em trabalho autónomo e nas várias componentes de avaliação. A percentagem de avaliação associada a estas competências deverá ser da ordem dos 15%.
Componente Laboratorial
Programação em Prolog. Utilização de model checkers e demonstradores automáticos.
Componente de Programação e Computação
Projeto computacional.
Princípios Éticos
Todos os membros de um grupo são responsáveis pelo trabalho do grupo. Em qualquer avaliação, todo aluno deve divulgar honestamente qualquer ajuda recebida e fontes usadas. Numa avaliação oral, todo aluno deverá ser capaz de apresentar e responder a perguntas sobre toda a avaliação.