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: 2018/2019 - 2S

Ativa?	Sim
Página Web:	http://www.dcc.fc.up.pt/~sandra/Home/TAL1819.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	9	PE a partir do ano letivo de 2014	1	-	6	42	162
MI:ERS	5	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 sem exame final

Componentes de Avaliação

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

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	60,00
Frequência das aulas	50,00
Trabalho escrito	40,00
Total:	150,00

Obtenção de frequência

Não existem condições de frequência.

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

Primeiro teste (50% de peso na nota final).
Segundo teste (50% de peso na nota final).
Sendo PT a classificação obtida  no primeiro teste e ST a
classificação obtida no segundo teste, então a nota final é dada por:
F = PT*(0.5) + ST*(0.5)
PT,ST >= 6 e F >= 9.5
Não obterão aprovação na avaliação distribuída, os alunos que não obtiverem um mínimo de 6 valores (em 20) em cada teste. Para os alunos que não obtiverem aprovação, haverá um exame de recurso cotado para 20 valores.

Provas e trabalhos especiais

A definir mais tarde.

Trabalho de estágio/projeto

A definir mais tarde.

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. O exame de melhoria de nota é classificado para 20 valores.