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
Carlos Augusto Isaac Piló Viegas Damásio, Ricardo João Rodrigues Gonçalves
Horas
Semanais - 5
Totais - 66
Idioma de ensino
Português
Pré-requisitos
N/A
Bibliografia
A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity. Shawn Hedman. Oxford Texts in Logic, 2004.
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.
Jon Barwise and John Etchemendy.
CSLI Publications, 2003.
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 demosntração coerentes, sistemas de prova coerentes e completos), sendo estes conceitos ilustrados com vários exemploes 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
- Média aritmética das notas dos 3 testes, arredondada às unidades, ou
- Nota do exame de recurso
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:
definição indutiva de linguagem proposicional
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