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 2013

Horário e local

Turma 2C (Sala D-004) 

  2^a Feira, de 08h às 10h

  4^a Feira, de 10h às 12h

Professores

Ruy José Guerra Barretto de Queiroz.

ATENÇÃO: Rede Social

(a ser anunciada).

Monitores

Natália Paola de Vasconcelos Cometti (Coordenadora)

Bertha Maria Correia Andaluz

Bruno Soares da Silva

George Harrison Álvares de Oliveira

Guilherme Palma Peixoto

João Gabriel Santiago Mauricio de Abreu

João Pedro de Carvalho Magalhães

Maria Gabriela Cardoso

Pedro Henrique Tôrres Gonçalves

Rafael Acevedo de Aguiar

Vinícius de Moraes Rego Cousseau

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 trabalhos práticos:
Tarski's World - Revised and Expanded, Dave Barker-Plummer, Jon Barwise and John Etchemendy In collaboration with Albert Liu, CSLI Publications, 2007, ISBN 1575864843. (Acompanha o software educativo Tarski's World)

Programação de Aulas

21-Out
Apresentação do Curso
Preliminares Matemáticos

28-Out
Exibição do video-clip Great Scientists: Aristotle, Allan Chapman
Preliminares Conceituais: Objetos e Predicados
A Lógica de Aristóteles: Lógica Aristotélica

30-Out
A Abordagem Algébrica de Boole
A Lógica Simbólica de Frege

04-Nov
Conjuntos Indutivamente Definidos

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

11-Nov
Conjuntos Livremente Gerados

13-Nov
Teorema da Extensão Homomórfica Única

18-Nov
Definição por Recursão sobre Conjuntos Indutivos

20-Nov
Provas por Indução sobre Conjuntos Indutivos

25-Nov
Lógica Proposicional: Semântica
Valoração-Verdade
Tabela-Verdade
O Conceito de Satisfatibilidade

27-Nov
Busca de Valoração: Método dos Tableaux

02-Dez
Método da Resolução

04-Dez
Dedução Natural (Gentzen)
Noção de Prova Formal (Gentzen)

09-Dez
Normalização de Provas

11-Dez
Cálculo de Seqüentes

16-Dez
Teorema da Compaccidade (Finitude)

18-Dez
Primeira Prova

06-Jan
Lógica de Primeira Ordem
Estruturas

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

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

15-Jan
Lógica de Primeira Ordem: Sintaxe e Semântica
Forma Prenex

20-Jan
Forma Normal de Skolem

22-Jan
Algoritmo da Unificação

27-Jan
Resolução para Primeira Ordem

29-Jan
Teorema de Herbrand

03-Fev
Teorema de Löwenheim-Skolem

05-Fev
Sistemas Axiomáticos (Euclides, Hilbert)
Completude, Incompletude

10-Fev
Aritmética de Peano

12-Fev
Funções recursivas primitivas

17-Fev
Funções recursivas parciais

19-Fev
Conjuntos recursivamente enumeráveis

24-Fev
Incompletude da Aritmética (Gödel)

26-Fev
Segunda Prova e entrega dos Exercícios do Tarski's World

10-Mar
Segunda Chamada

12-Mar
Prova Final 

Última atualização: 03 Novembro 2013, 01:30pm GMT-3