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

Método de Avaliação: 50% exame, 50% projeto

Tipo

Não Estruturante

Regime

Semestral

Carga Horária

1º Semestre

3.0 h/semana

1.5 h/semana

147.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

Método de Avaliação: 50% exame, 50% projeto

Pré-requisitos

Componente Laboratorial

Princípios Éticos

Componente de Programação e Computação

Componente de Competências Transversais

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


Several additional papers

Another

Another

Another