1. Início
  2. Faculdade de Ciências e Tecnologia
  3. Engenharia Informática
  4. Lógica Computacional

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

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

A avaliação poderá ser realizada através de três 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.
 
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:
  1. Média aritmética das notas dos 3 testes, arredondada às unidades, ou
  2. Nota do exame de recurso
 
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:
     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

Cursos

Cursos onde a unidade curricular é leccionada: