Programa

Algoritmos para Lógica Computacional

Mestrado Bolonha em Matemática e Aplicações e Computação

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

Mestrado Bolonha em Engenharia Informática e de Computadores - Taguspark

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.