Lógica Computacional
Objetivos
Conhecimento
- Sintaxe e a semântica da lógica proposicional e de primeira ordem
- Método de resolução para a lógica proposicional e de primeira ordem
- Sistemas de dedução natural da lógica proposicional e de primeira ordem
Aptidões
- Escrever fórmulas lógicas a partir de descrições em língua natural
- Calcular semântica, axiomática, e sintaticamente a validade lógica de fórmulas
- Usar resolução para estabelecer a validade lógica de fórmulas
Competências
- Capacidade de raciocínio abstracto e rigoroso
- Capacidade de manipulação de estruturas formais
- Aprender a aprender
Caracterização geral
Código
7336
Créditos
6.0
Professor responsável
João Alexandre Carvalho Pinheiro Leite, Ricardo João Rodrigues Gonçalves
Horas
Semanais - 5
Totais - 70
Idioma de ensino
Português
Pré-requisitos
N/A
Bibliografia
Referências principais:
A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity. Shawn Hedman. Oxford Texts in Logic, 2004.
Mathematical Logic.
Ian Chiswell and Wilfrid Hodges. Oxford Texts in Logic, 2007.
Slides e exercícios.
Depois de cada aula, os slides e os exercícios serão disponibilizados online no CLIP.
Leitura complementar:
Lógica Computacional: Proposicional e de 1ª ordem. Apontamentos de Paula Gouveia e F. Miguel Dionísio. Instituto Superior Técnico.
Logic in Computer Science: modelling and reasoning about systems.
Michael Huth and Mark Ryan.
Cambridge University Press, 2004.
Language, Proof and Logic (2nd edition).
Dave Barker-Plummer, Jon Barwise and John Etchemendy.
CSLI Publications, 2011.
Método de ensino
Há três horas de aulas teóricas e duas horas de aulas práticas por semana.
Nas aulas teóricas abordam-se os conceitos fundamentais da lógica computacional (nomeadamente linguagens proposicionais e de 1ª ordem, interpretações e validade, regras de demonstração coerentes, sistemas de prova coerentes e completos), sendo estes conceitos ilustrados com vários exemplos e dois sistemas formais: Dedução Natural mais próximo do raciocínio humano e Resolução, mais apropriado a implementação computacional.
Nas aulas práticas, os alunos aplicam estes conceitos em vários problemas que lhes são propostos, que embora simples, os obriga a utilizar o conhecimento exposto nas aulas teóricas e a consolidar o raciocínio abstrato e rigoroso.
Método de avaliação
A avaliação poderá ser realizada através de dois testes, em datas a indicar no CLIP, cada um requerendo inscrição prévia. Os testes são classificados com uma nota de 0 a 20 valores, arredondada à primeira casa decimal.
Em alternativa, a avaliação poderá ser realizada através de um exame na época de recurso, em data a indicar no CLIP. O exame é classificado com uma nota de 0 a 20 valores, arredondada à primeira casa decimal.
Tantos os testes como o exame serão realizados presencialmente, são sem consulta, e não é permitida a utilização de qualquer dispositivo eletrónico durante a sua realização.
A nota final é obtida através de:
- Média aritmética das notas dos 2 testes, arredondada às unidades, ou
- Nota do exame de recurso, arredondada às unidades
Obtém aprovação o aluno que tiver nota final igual ou superior a 10.
Conteúdo
Lógica Proposicional
Sintaxe:
definição indutiva de linguagem proposicional
termos a partir de descrições em linguagem natural
Semântica:
tabelas de verdade
valoração e estrutura de interpretação: relação de satisfação
validade e consequência logica; equivalência
Sistema dedutivo: dedução natural
regras de introdução e eliminação
derivação e prova
correcção e completude
Algoritmo de decisão
Forma normal conjuntiva e forma clausal
Resolução
Lógica de primeira ordem
Sintaxe:
alfabeto e linguagem de primeira ordem
termos a partir de descrições em linguagem natural
variáveis livres e substituição
Semântica:
valoração e estrutura de interpretação: relação de satisfação
validade e consequência logica; equivalência
Sistema dedutivo: dedução natural
regras de introdução e eliminação
derivação e prova
correcção e completude (esboço)
Algoritmo de decisão
Skolemização e unificação
Resolução
Programação em Lógica
Prolog