Tópicos Avançados em Lógica

Código:

CC4026

Sigla:

CC4026

Nível:

400

Áreas Científicas
Classificação	Área Científica
OFICIAL	Ciência de Computadores

Ocorrência: 2017/2018 - 2S

Ativa?	Sim
Página Web:	http://www.dcc.fc.up.pt/~sandra/Home/TAL1718.html
Unidade Responsável:	Departamento de Ciência de Computadores
Curso/CE Responsável:	Mestrado em Ciência de Computadores

Ciclos de Estudo/Cursos

Sigla	Nº de Estudantes	Plano de Estudos	Anos Curriculares	Créditos UCN	Créditos ECTS	Horas de Contacto	Horas Totais
M:CC	4	PE a partir do ano letivo de 2014	1	-	6	42	162
MI:ERS	6	Plano Oficial desde ano letivo 2014	4	-	6	42	162

Língua de trabalho

Português - Suitable for English-speaking students

Objetivos

Aplicação de tópicos avançados de lógica na resolução de problemas em várias áreas de ciência de computadores.

Resultados de aprendizagem e competências

Pretende-se que o aluno:
- perceba a importância da utilização da lógica e dos sistemas formais na resolução de problemas concretos;
- seja capaz de modelar problemas concretos em diferentes sistemas de lógica e resolvê-los utilizando ferramentas adequadas (SAT e SMT solvers);
- seja capaz de relacionar teoria de prova com programação em diversos paradigmas (com enfase para o funcional e lógico).

Modo de trabalho

Presencial

Pré-requisitos (conhecimentos prévios) e co-requisitos (conhecimentos simultâneos)

Conhecimentos básicos de lógica, equivalentes a um curso standard de lógica de uma licenciatura.

Programa

- Lógica intuicionística: lógica proposicional; dedução natural; relações entre a lógica clássica e intuicionistica; teoria de tipos; termos-prova; provas como programas (o isomorfismo de Curry-Howard); reduções como regras de computação; programação funcional; lógica intuicionística de primeira ordem; números naturais; definições indutivas.
- Resolutores SAT: lógica proposicional; problemas de decisão SAT e VAL; formas normais; equisatifabilidade; codificação de Tseitin; algoritmos de resolução SAT (conceitos básicos); Framework DPLL e suas optimizações; modelação de problemas concretos em lógica proposicional e resolução usando um resolutor SAT;
- Resolutores SMT: lógica proposicional de primeira ordem(FOL);
problemas de decisão SAT e VAL; formas normails (Herbrantização e Skolemização); FOL com igualdade.  Teorias de primeira ordem: conceitos básicos e problemas de decidibilidade; diferentes teorias (igualdade, inteiros, aritmética linear; reais ; arrays); combinação de teorias; satisfabilidade módulo teorias; resolutores SMT; SMT-LIB; aplicações.

Bibliografia Obrigatória

Kroening Daniel; Decision procedures. ISBN: 9783540741046
Goubault-Larrecq Jean; Proof theory and automated deduction. ISBN: 978-0-7923-4593-0

Bibliografia Complementar

Morten Heine Sørensen and Pawel Urzyczyn; Lectures on the Curry-Howard Isomorphism, Elsevier Science, 2006. ISBN: 978-0444520777
Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X

Métodos de ensino e atividades de aprendizagem

Aulas expositivas e resolução de problemas e casos de estudo.

Tipo de avaliação

Avaliação distribuída com exame final

Componentes de Avaliação

Designação	Peso (%)
Exame	50,00
Teste	50,00
Total:	100,00

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	50,00
Frequência das aulas	50,00
Total:	100,00

Fórmula de cálculo da classificação final

A classificação final é calculada como média aritmética de um teste a meio do semestre e um segundo teste a realizar na época normal de exames.

Melhoria de classificação

Os alunos que não tiveram aprovação através da realização dos dois testes, ou que queiram melhorar a classificação obtida, podem fazê-lo na época de recurso.