Disciplina

Área

Área Científica de Metodologia e Tecnologias da Programação > Algoritmos

Activa nos planos curriculares

MMA 2006 > MMA 2006 > 2º Ciclo > Perfis > Matematica da Computação > Metodologia e Tecnologia da Programação > Opções - Mtp > Algoritmos para Lógica Computacional

MEIC-T 2021 > MEIC-T 2021 > 2º Ciclo > Área Principal > Agrupamentos > Algoritmos e Aplicações > Algoritmos para Lógica Computacional

MEIC-T 2015 > MEIC-T 2015 > 2º Ciclo > Agrupamentos > Algoritmos e Programação > Algoritmos para Lógica Computacional

GENI > GENI > 1º Ciclo > Área Principal > Percursos > Percurso Livre > Opções 1 > Algoritmos para Lógica Computacional

MEIC-A 2021 > MEIC-A 2021 > 2º Ciclo > Area Principal > Agrupamentos > Algoritmos e Aplicações > Algoritmos para Lógica Computacional

MEIC-A 2015 > MEIC-A 2015 > 2º Ciclo > Agrupamentos > Algoritmos e Programação > Algoritmos para Lógica Computacional

Nível

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.

Tipo

Não Estruturante

Regime

Semestral

Carga Horária

1º Semestre

2.0 h/semana

1.5 h/semana

119.0 h/semestre

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.

Pré-requisitos

Facilidade de programação numa das seguintes linguagens de programação: C, Python ou Java. Conhecimentos básicos de algoritmia, estruturas de dados e lógica.

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.

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.

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.

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.

Bibliografia

Principal

Handbook of Satisfiability

A. Biere, M. Heule, H. van Maaren and T. Walsh

2009

IOS Press


Secundária

Handbook of Knowledge Representation

F. Van Harmelen, Vladimir Lifschitz, and Bruce Porter

2008

Elsevier


Handbook of Constraint Programming

F. Rossi, Peter Van Beek, and Toby Walsh

2006

Elsevier