Lógica Computacional

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

Caracterização geral

Código

7336

Créditos

6.0

Professor responsável

A disponibilizar brevemente

Horas

Semanais - A disponibilizar brevemente

Totais - 66

Idioma de ensino

Português

Pré-requisitos

A disponibilizar brevemente

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.

• 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, 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.
              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

Cursos

Cursos onde a unidade curricular é leccionada: