Lógica Computacional
Código
7336
Unidade Orgânica
Faculdade de Ciências e Tecnologia
Departamento
Departamento de Informática
Créditos
6.0
Professor responsável
Pedro Manuel Corrêa Calvente Barahona
Horas semanais
5
Total de horas
72
Língua de ensino
Português
Objectivos
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
Pré-requisitos
Não tem. É uma disciplina introdutória do início do curso.
Conteúdo
Lógica Proposicional
Sintaxe:
Termos a partir de descrições em linguagem natural
Conectores lógicos
Definição indutiva de linguagem proposicional
Formas Normais: Negativa, Conjuntiva e Disjuntiva
Semântica:
Tabelas de verdade e álgebra de Boole
Valoração e estrutura de interpretação: relação de satisfação
Validade e consequência lógica; equivalência
Sistema dedutivo: dedução natural
Regras de introdução e eliminação
Derivação e prova
Coerência e Completude
Sistema dedutivo: resolução
Forma normal conjuntiva e forma clausal
Algoritmo de Horn
Resolução e Refutação
Lógica de primeira ordem
Sintaxe:
Termos a partir de descrições em linguagem natural
Alfabeto e Definição indutiva de linguagem de 1ª ordem
Variáveis livres e substituição
Semântica:
Valoração e estrutura de interpretação: relação de satisfação
Validade e consequência lógica; equivalência
Sistema dedutivo: dedução natural
Regras de introdução e eliminação
Derivação e prova
Sistema dedutivo: resolução
Forma Normal de Skolem e skolemização
Unificação e resolução
Inferência por Indução Estrutural
Estruturas Indutivas
Exemplos:
Definição Indutiva de linguagem proposicional
Listas e árvores
Números naturais
Indução Estrutural
Exemplos
Bibliografia
Principal livro de texto:
Language Proof and Logic (4th edition).
Jon Barwise and John Etchemendy.
CSLI Publications, 2003.
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
O ensino da disciplina é baseado quer no livro de texto recomendado quer no software de apoio que o acompanha.
Nas aulas teóricas é exposta a matéria e nas aulas práticas são resolvidos problemas, a maioria dos quais com o apoio do software referido.
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 a sintaxe e a semântica e sistemas de dedução da lógica proposicional. Analogamente, os 3º e o 4º testes cobrem a lógica de predicados de 1ª ordem e a inferência por indução estrutural.
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.
Nac = (T1+T2+T3+T4)/4.
Recurso
O aluno reprovado na avaliação contínua pode fazer um exame de Recurso, com classificação (Nr) de 0 a 20. Neste caso, a nota final obtida é o máximo das notas de avaliação contínua e de recurso.
NF = max(Nac, Nr)
Frequência.
Não há avaliação para obtenção de frequência. Todos os alunos são admitidos aos testes/exame.