Disciplina Curricular

Algoritmos para Lógica Computacional ALC

Mestrado Bolonha em Engenharia Informática e de Computadores - Alameda - MEIC-A 2021

Contextos

Grupo: MEIC-A 2021 > 2º Ciclo > Area Principal > Agrupamentos > Algoritmos e Aplicações

Período:

Peso

6.0 (para cálculo da média)

Objectivos

A Lógica é um dos pilares da Ciência da Computação (Computer Science, CS), encontrando aplicação em todas as áreas de CS. Exemplos concretos incluem as bases de dados, os sistemas de informação inteligentes, a inteligência artificial, mas também a especificação, validação e verificação de software, hardware e redes. O objectivo desta unidade curricular é proporcionar formacão avançada em abordagens para resolver problemas computacionais relacionados com Lógica. Os estudantes ficam capacitados para analisar, modelar e resolver problemas computacionalmente difíceis usando Lógica. Adicionalmente, obtém formação nos aspectos de engenharia essenciais na construção de software para problemas de Lógica: funcionamento e implementação de um sistema dedutivo e técnicas algorítmicas e estruturas de dados fundamentais para a implementação de ferramentas baseadas em Lógica.

Programa

Problemas de decisão em lógica proposicional (Boolean Satisfiability, SAT). Exemplos de modelação com lógica proposicional. Algoritmos para SAT. Problemas de decisão em lógica de primeira ordem. O problema de Satisfação Módulo Teorias (Satisfiability Modulo Theories, SMT). Conversão para SAT. Algoritmos para SMT. A Programação por Restrições (Constraint Programming, CP): Algoritmos e exemplos de modelação. Conversão de e para lógica proposicional. Programação por Conjuntos de Resposta (Answer Set Programming, ASP): algoritmos e exemplos de modelação. Relação com a lógica proposicional. Problemas de função e enumeração para SAT, SMT, ASP e CP, incluindo problemas de optimização e problemas relacionados com conjuntos sobre-especificados de restrições. Problemas de decisão, de função e de enumeração com variáveis proposicionais quantificadas. Exemplos de aplicação.     

Metodologia de avaliação

Existe uma componente laboratorial (L) e uma componente teórica (T). A componente L corresponde à média dos projectos. A componente T corresponde a um exame. A nota final é a média de L e T, i.e. (T+P)/2. Ambas as componentes L e T têm a nota mínima de 8 valores.

Componente de Competências Transversais

Esta unidade curricular fomenta o pensamento crítico e inovador atavés da análise e proposta de resolução para diversos problemas. A componente de projecto não é fechada, estimulando a criatividade dos alunos na procura de novas e melhores soluções. Adicionalmente, os projectos são realizados em grupo, obrigando a um trabalho em equipa para o seu sucesso.

Componente Laboratorial

As aulas laboratoriais são dedicadas à resolução de problemas usando modelos nos paradigmas apresentados nas aulas teóricas. Estas também são parcialmente dedicadas a ajudar os alunos nos projectos.

Componente de Programação e Computação

No curso onde esta UC é oferecida estão asseguradas as componentes de Computação e Programação de acordo com o MEPP 2122.

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.

Disciplinas Execução

2021/2022 - 1º Semestre