Lógica Computacional

Imagem d@ Sebastião Pais [Ficheiro Local]
Sebastião Pais
Código:
16673
Ano:
2
Semestre:
S1
Créditos ECTS:
6
Carga Horária:
PL(30H)/T(30H)
Área Científica:
Informática
Tipo de ensino:
Presencial.
Estágios:
Não aplicável.
Objectivos de Aprendizagem:
No final da Unidade Curricular, o(a) estudante deve ser capaz de:
1. Formalizar problemas em lógica proposicional e de primeira ordem e analisar satisfazibilidade, validade e consequência lógica.
2. Aplicar a forma clausal, a unificação e a resolução SLD na construção e na verificação de provas.
3. Desenvolver programas em Prolog, explicando o modelo de execução (árvore de procura, retrocesso) e usando o corte e a negação por falha.
4. Manipular listas, árvores, grafos e gramáticas DCG com recursão e acumuladores.
5. Descrever a semântica de ponto fixo do Datalog e aplicá-la a dados relacionais e grafos de conhecimento.
6. Modelar e resolver problemas combinatórios em Answer Set Programming, com restrições e otimização.
No final, o(a) estudante deverá ter adquirido as competências necessárias para integrar raciocínio simbólico em sistemas de IA capazes de justificar as suas conclusões e discutir o papel da lógica na IA neuro-simbólica.
Conteúdos programáticos:
1. Fundamentos de lógica para a computação: lógica proposicional (sintaxe, semântica, tabelas de verdade); satisfazibilidade, validade e consequência lógica; formas normais e SAT solvers; lógica de primeira ordem.
2. Dedução automática: cláusulas de Horn; princípio da resolução; unificação e unificador mais geral; árvores de prova; resolução SLD.
3. Programação lógica e Prolog: factos, regras e questões; árvore de procura e retrocesso; aritmética, entrada/saída e predicados pré-definidos; corte e negação por falha.
4. Estruturas de dados e técnicas declarativas: listas, acumuladores e diferenças de listas; árvores e grafos; avaliação de expressões; autómatos finitos; gramáticas DCG.
5. Datalog e raciocínio sobre dados: semântica de ponto fixo; negação estratificada; bases de dados dedutivas e grafos de conhecimento.
6. Programação lógica e IA: Answer Set Programming (modelos estáveis e agregados, e otimização); programação lógica indutiva; raciocínio neuro-simbólico.
Metodologias de Ensino e Critérios de Avaliação:
Os conteúdos desta unidade curricular são expostos em aulas teóricas (métodos expositivos e interativos) e a sua vertente prática é explorada em aulas laboratoriais. Cada tipo de aula tem duas horas de contacto por semana.
As aulas práticas regem-se por guias e fichas laboratoriais que os estudantes executam nos computadores dos laboratórios. Os trabalhos individuais e de grupo propostos são concebidos de modo a que os alunos desenvolvam as capacidades técnicas descritas nos objetivos através do projeto e da implementação de laboratórios. Avaliam-se as componentes teóricas e práticas recorrendo a 2 elementos principais:
- Fichas práticas 50% - 10 Valores;
- Testes escritos 50% - 10 Valores.
Bibliografia principal:
Material de ensino:
Disponibilizado na página da UC no Moodle.

Livros:
Mordechai Ben-Ari. Mathematical Logic for Computer Science. Springer, 3rd edition, 2012.
Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and reasoning about systems. CUP, 2004.
Jon Barwise and John Etchmendy. Language, Proof, and Logic. CSLI, 2nd Edition, 2011.
D. van Dalen. Logic and Structure. 5th Edition, Springer Verlag, Berlin, Germany, 2013.

Adicional:
-Shawn Hedman. A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity. Oxford Texts in Logic, 2004.
Língua:
Português
Esta informação promove os seguintes Objetivos de Desenvolvimento Sustentável da ONU:
Garantir o acesso à educação inclusiva, de qualidade e equitativa, e promover oportunidades de aprendizagem ao longo da vida para todos Garantir padrões de consumo e de produção sustentáveis