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: 2014/2015 - 2S

Ativa?	Sim
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	0	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

- SAT solvers: propositional logic; decision problems SAT and VAL; normal forms; equisatisfiability; Tseitin's encoding; SAT solving algorithms (basic concepts); DPLL framework and its optimisations; modeling concrete problems in propositional logic and solving using a SAT solver.
- SMT solver: classical first order logic (FOL); decision problems SAT and VAL; normal forms (Herbrandization and Skolemization); FOL with equality; many-sorted FOL. First order theories: basic concepts and decidability issues; several theories (equality, integers, linear arithmetic, reals, arrays); combining theories; satisfiability modulo theories; SMT solvers; SMT-LIB; applications.
- Intuitionistic Logic: propositional logic; natural deduction; connections between classical and intuitionistic logic; type theory; proof terms; proofs as programs (Curry-Howard isomorphism); reductions as rules of computation; functional programming; first-order intuitionistic logic; natural numbers; inductive definitions.
- Sequent calculus: cut-elimination; theorem proving; proof search; computation as proof search; goal-directed search; definite clauses; resolution.

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.