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
Pedro Manuel Corrêa Calvente Barahona
Horas
Semanais - 6
Totais - 66
Idioma de ensino
Português
Pré-requisitos
N/A
Bibliografia
Principal livro de texto:
• Language, Proof, and Logic, David Barker-Plummer, Jon Barwise, John Etchemendy, Center for the Study of Language and Information; 2nd edition, October 2011.
Literatura adicional:
• Mathematical Logic: a course with exercices. Part I: propositional calculus, boolean algebras, predicate calculus, René Cori e Daniel Lascar, Oxford Press, 2007.
• A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity, Shawn Hedman, Oxford Texts in Logic, 2004.
• Logic in Computer Science: modelling and reasoning about systems (2nd edition), Michael Huth and Mark Ryan, Cambridge University Press, 2004
Método de ensino
Há duas horas de aulas teóricas e três 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 demosntarção 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 proplemas 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 é feita através de 4 testes, cada um com duração de 1 hora, ou através de exame de recurso. O 1º e o 2º testes cobrem basicamente a lógica proposicional, e os 3º e o 4º testes cobrem a lógica de predicados de 1ª ordem e a inferência por indução estrutural.
Os testes e o exame são feitos presencialmente e sem consulta.
• Aprovação.
O aluno que obtenha uma nota positiva na avaliação contínua (Nac >= 10) obtem aprovação com essa nota final (Nf). A nota da avaliação contínua é obtida pela média aritmética dos 4 testes, avaliados de 0 a 20, arredondadas às centésimas)
Nac = (T1+T2+T3+T4)/4.
• Recurso
O aluno reprovado na avaliação contínua pode fazer um exame de Recurso, estruturado em quatro grupos, correspondentes aos testes da avaliação contínua, cada qual classificado de de 0 a 20. Neste caso, a nota final obtida é a média aritmética do máximo das notas de avaliação contínua e de recurso nos vários testes/grupos, arredondadas às centésimas.
Nf = (max(T1,G1)+max(T2,G2)+max(T3,G3)+max(T4,G4)) / 4
• Melhoria
O aluno que tenha obtido aprovação nesta edição da disciplina e pretenda fazer melhoria através do exame de recurso, terá uma nota final, Nm, obtida da mesma forma.
Nm = (max(T1,G1)+max(T2,G2)+max(T3,G3)+max(T4,G4)) / 4
O aluno com aprovação em edição anterior da disciplina com nota Na, e que faça o exame de recurso para melhorar essa nota, obterá como nota final o máximo da nota anterior e da nota no exame.
Nm = max(Na, (T1+T2+T3+T4)/4 )
• Frequência.
Não há avaliação para obtenção de frequência. Todos os alunos são admitidos aos testes/exame.
Conteúdo
1. Lógica Proposicional
1.1. Sintaxe:
• Definição indutiva de linguagem proposicional
1.2. Semântica:
• Tabelas de verdade e álgebra de Boole
• Valoração e estrutura de interpretação: satisfação
• Validade e consequência lógica; equivalência
1.3. Algoritmos de Decisão e Sistemas de Prova
• Dedução natural: Regras de introdução e eliminação
• Resolução: Forma clausal, Algoritmos de Horn
2. Lógica de primeira ordem
2.1. Sintaxe:
• Termos e Linguagem de 1ª ordem
• Tradução de descrições em língua natural
• Variáveis livres e substituição
2.2. Semântica:
• Valoração e estrutura de interpretação: satisfação
2.3. Algoritmos de Decisão e Sistemas de Prova:
• Resolução: Skolemização, Unificação
• Dedução natural: Regras de introdução e eliminação
3. Indução Matemática