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

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 demonstração coerentes, sistemas de prova coerentes e completos), sendo estes conceitos ilustrados com vários exemplos 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 dois 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 2 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
  Programação em Lógica
    Prolog

Cursos

Cursos onde a unidade curricular é leccionada: