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 2005

Horário e local

Turmas 2C e 2E (Sala 8)
  2a Feira, de 10h às 13h
  4a Feira, de 07h às 10h

Professor

Ruy José Guerra Barretto de Queiroz.

Monitores

Aluisio Rodrigo Fonseca de Santana (arfs)
Eduardo Wagner Marques de Almeida (ewma)
Fernando Valente Kakimoto (fvk)
Francisco Paulo Magalhães Simões (fpms)
Icamaan Botelho Viegas da Silva (ibvs)
Joao Victor Guimarães de Lemos (jvgl)
José Benito Fernandes de Araújo Neto (jbfan)
Luiz Carlos Assis DOleron Barreto (lcadb)
Nancy de Lyra Lino (nll)
Nicole Barbosa Sultanum (nbs2)
Pablo Alessandro Barbosa Viana (pabv)
Rebeka Gomes de Oliveira (rgo2)
Roberto Cássio Silva do Nascimento Júnior (rcsdnj)
Thiago de Barros Lacerda (tbl2)

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 ps e em pdf), Dirk van Dalen
  • 2a. Unidade: Uma Teoria de Modelos mais Curta (em ps e 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

    Aula
    Data
    Assunto
    Horas Acum.
    1 19-set Apresentação do Curso
    Preliminares Matemáticos
    Preliminares Conceituais: Objetos e Predicados
    A Lógica de Aristóteles: Silogismos    		 03
    2 21-set Silogismos. Inferências Logicamente Seguras
    		 06
    3 26-set Simbolismo e Representação do Conhecimento (Leibniz)
    A Abordagem Algébrica de Boole
    A Lógica Simbólica de Frege
    Conjuntos Indutivamente Definidos     		09
    4 28-set Mini-Prova 12-13hs
    Conjuntos Indutivamente Definidos (cont.)
    Fecho Indutivo
    		 12
    5 03-out Provas por Indução sobre Conjuntos Indutivos
    Conjuntos Livremente Gerados
    Lógica Proposicional: Sintaxe Lógica Proposicional: Semântica
    Valoração-Verdade
    O Problema da Satisfatibilidade     		15
    6 05-out Mini-Prova 12-13hs
    Lógica Proposicional: Semântica (cont.):
    Tabela-Verdade, Satisfatibilidade
    Considerações sobre o Custo Computacional de SAT     		18
    7 10-out Busca de Valoração: Método dos Tableaux 21
      12-out FERIADO - Nossa Senhora Aparecida  
    8 17-out Entrega do Avaliador de Expressões
    Busca de Valoração: Método dos Tableaux (cont.)
    Método da Resolução     		24
    9 19-out Mini-Prova 12-13hs
    Método da Resolução (cont.)     		27
    10 24-out Noção de Prova Formal (Gentzen)
    Dedução Natural: Conjunção, Disjunção, Implicação     		30
    11 26-out Mini-Prova 12-13hs
    Dedução Natural: Negação     		33
    12 31-out Primeira Prova 36
    13 07-nov Teorema da Compaccidade (Finitude)
    Decidibilidade     		39
    14 09-nov Mini-Prova 12-13hs
    Estruturas de Primeira Ordem
    Funções entre Estruturas
    A Noção de Subestrutura     		42
    15 14-nov Termos e Fórmulas Atômicas
    Lógica de Primeira Ordem: Sintaxe e Semântica     		45
    16 16-nov Mini-Prova 12-13hs
    Linguagem vs Estruturas:
    Diagramas
    Modelos Canônicos     		48
    17 21-nov Forma Prenex
    Forma Normal de Skolem     		51
    18 23-nov Mini-Prova 12-13hs
    Algoritmo da Unificação     		54
    19 28-nov Resolução para Primeira Ordem
    Teorema de Herbrand     		57
      30-nov Semana Pedagógica  
    20 05-dez Sistemas Axiomáticos (Euclid, Hilbert) 60
    21 07-dez Aritmética de Peano
    Incompletude (Gödel)     		63
    22 12-dez Segunda Prova e entrega do Tarski 66
    23 14-dez Segunda Chamada 69
    24 19-dez Prova Final 72

    ATENÇÃO: Newsgroup

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

    Última atualização: 29 de Setembro de 2005, 16:32hs