Universidade Federal de Pernambuco (UFPE)
Centro de Informática (CIn)
Graduação em Ciência da Computação e Engenharia da Computação

IF673 - Lógica para Computação

Segundo Semestre de 2007

Horário e local

Turmas 2C e 2E (Sala D-005)
  2a Feira, de 10h às 12h
  4a Feira, de 8h às 10h

Professor

Ruy José Guerra Barretto de Queiroz.

ATENÇÃO: Newsgroup

Todas as mensagens relativas à disciplina são veiculadas no grupo de notícias depto.cursos.grad.if673.

Monitores

Eduardo Wagner Marques de Almeida (ewma) (Coordenador)
Andre Melo (afpm)
Flávia Renata Costa Chaves (frcc)
Yane Wanderley dos Santos Rodrigues (ywsr)
Victor Hugo Queiroz da Rocha (vhqr)

Regras gerais para condução da disciplina

aqui

Charadas

de Smullyan: aqui

Bibliografia (tradução (parcial) para o português de alguns itens da bibliografia)

  • 1a. Unidade: Lógica e Estrutura (em pdf, Capítulo 7), Dirk van Dalen
  • 2a. Unidade: Uma Teoria de Modelos mais Curta (em pdf), Wilfrid Hodges
  • Livro e CD (software) para aulas práticas:
    Language, Proof and Logic, Jon Barwise & John Etchemendy, CSLI Publications, 2002, ISBN 157586374X. (Acompanha o software educativo Tarski's World)

    Programação de Aulas

    17-Set
    Apresentação do Curso
    Preliminares Matemáticos

    19-Set
    Preliminares Conceituais: Objetos e Predicados
    A Lógica de Aristóteles: Silogismos

    24-Set
    A Abordagem Algébrica de Boole
    A Lógica Simbólica de Frege

    26-Set
    (Mini-Prova)
    Conjuntos Indutivamente Definidos

    01-Out
    Fecho Indutivo
    (Ver capítulo 2, seção 2.3, do livro de J. Gallier: aqui)

    03-Out
    (Mini-Prova)
    Provas por Indução sobre Conjuntos Indutivos
    Conjuntos Livremente Gerados
    Teorema da Extensão Homomórfica Única

    08-Out
    Lógica Proposicional: Sintaxe
    Lógica Proposicional: Semântica
    Valoração-Verdade
    Tabela-Verdade

    10-Out
    O Conceito de Satisfatibilidade

    15-Out
    O Problema SAT e correlatos

    17-Out
    (Mini-Prova)
    Busca de Valoração: Método dos Tableaux

    22-Out
    Busca de Valoração: Método dos Tableaux (cont.)

    24-Out
    Método da Resolução

    29-Out
    (Mini-Prova)
    Dedução Natural (Gentzen)

    31-Out
    Noção de Prova Formal (Gentzen)

    05-Nov
    Teorema da Compaccidade (Finitude)

    07-Nov
    Primeira Prova

    12-Nov
    Funções entre Estruturas: Homomorfismos, Imersões
    A Noção de Subestrutura

    14-Nov
    Termos e Fórmulas Atômicas
    Linguagem vs Estruturas: Diagramas e Modelos Canônicos

    19-Nov
    Lógica de Primeira Ordem: Sintaxe e Semântica
    Forma Prenex

    21-Nov
    Forma Normal de Skolem

    26-Nov
    (Mini-Prova)
    Algoritmo da Unificação

    28-Nov
    Resolução para Primeira Ordem

    03-Dez
    Teorema de Herbrand

    05-Dez
    Teorema da Compaccidade

    10-Dez
    Teorema da Compaccidade (cont.)

    02-Jan
    Sistemas Axiomáticos (Euclides, Hilbert)
    Completude, Incompletude
    Aritmética de Peano

    07-Jan
    Funções recursivas primitivas

    09-Jan
    Funções recursivas parciais

    14-Jan
    (Mini-Prova)
    Conjuntos recursivavemente enumeráveis

    16-Jan
    Incompletude da Aritmética (Gödel)

    21-Jan
    Incompletude da Aritmética (cont.)

    23-Jan
    Segunda Prova e entrega do Tarski

    28-Jan
    Segunda Chamada

    30-Jan
    Prova Final

    Última atualização: 02 de Janeiro de 2008, 12:51pm GMT-3