Lógica para computação (2006/1)

Seja n o número inteiro mínimo que não tem descrição em menos que 20 palavras.

Bem-vindo à lógica.

Informações gerais

Carga horária: 60 h (em 30 aulas de 2h)
Créditos: 4
Súmula: Lógica sentencial e de primeira ordem. Sistemas dedutivos naturais e axiomáticos. Completeza,consistência e correção. Formalização de problemas. Formalização de programas e sistemas de computação simples.
Turma: A
Horário/Sala: Terça 08:30-10:10 e quinta 08:30-10:10 na sala 111 do prédio 43425 (vê também aqui).
Consultas: Quarta 15-17.
Detalhes: Vê o programa.

Datas importantes

A disciplina começa no dia 07/03/2006.
Entrege o trabalho 1 até o dia 06/04/2006.
Prova 1 vai ser realizado no dia 18/04/2006.
Prova 2 vai ser realizado no dia 01/06/2006.
A apresentação dos trabalhos vai ser realizada nos dia 08 e 13 do junho.

Resultados

Materiais

Página da disciplina em 2005/1 por Aline Vieira Malanovicz.
Página da disciplina por Luís da Cunha Lamb.
Página da disciplina por Juliana Kaizer Vizzotto.

Aulas

Aqui se acha uma versão dos slides das aulas (handout em preto e branco) junto com os exercícios.

No.	Data	Tópicos	Material
1	07/03/2006	Administrativa, Introdução.	Slides
2	09/03/2006	Dedução natural: Regras de prova e exemplos 1.	Slides, Exercícios 1, Soluções 1
3	14/03/2006	Dedução natural: Regras de prova e exemplos 2.	Slides
4	16/03/2006	Dedução natural: Exemplos e leis importantes.	Slides, Exercícios 2, Soluções 2
5	21/03/2006	Dedução natural: Leis importantes. O sistema de Hilbert.	Slides
6	23/03/2006	Semântica da lógica propositional.	Slides, Exercícios 3, Soluções 3
7	28/03/2006	Indução matemática.	Slides
8	30/03/2006	Consistência e completude da lógica propositional.	Slides, Trabalho 1, Solução trabalho 1
9	04/04/2006	Árvores de refutação. Introdução e exemplos.	Slides
10	06/04/2006	Árvores de refutação. Formas normais.	Slides, Exercícios 4, Soluções 4
11	11/04/2006	História e lógicas não-classicas.	Slides
12	13/04/2006	Revisão da primeira parte.
13	18/04/2006	Prova 1	Prova 1, Soluções prova 1
14	20/04/2006	Resultados da prova 1.
15	25/04/2006	Introdução à lógica de predicados.	Slides
16	27/04/2006	Introdução à lógica de predicados. Linguagem formal.	Slides, Exercícios 6, Soluções 6
17	02/05/2006	Semântica da lógica de predicados.	Slides, Proposta de trabalhos
18	04/05/2006	Semântica da lógica de predicados.	Slides, Exercícios 7, Soluções 7
19	09/05/2006	Semântica da lógica de predicados. Introdução a dedução natural.	Slides
20	11/05/2006	Dedução natural: Regras e exemplos.	Slides, Exercícios 8, Soluções 8
21	16/05/2006	Dedução natural: Regras e exemplos.	Slides
22	18/05/2006	Dedução natural: Teoremas importantes.	Slides
23	23/05/2006	Dedução natural: Exemplos. Árvores de refutação: Regras e exemplos.	Slides
24	25/05/2006	Arvóres de refutação: Regras e exemplos.	Slides, Exercícios 9, Soluções 9
25	30/05/2006	Árvores de refutação: Exemplos. Revisão para prova 2.
26	01/06/2006	Prova 2	Prova 2, Soluções prova 2
27	06/06/2006	Resultados da prova 2.
28	08/06/2006	Apresentação dos trabalhos.
29	13/06/2006	Apresentação dos trabalhos.
	15/06/2006	Feriado: Corpus_Cristi
30	20/06/2006	Visão geral, lógica de segunda ordem, complexidade, Administrativa	Slides
	27/06/2006	Revisão, exercícios e perguntas.	Exercícios 10, Soluções 10
	04/07/2006	Prova de recuperação	Prova

Suplementos

George Boole: An investigation of the laws of thought.

Texto antigo seminal, para quem tem interesse de ter uma impressão como a lógica moderna começou. Cuidado: A notação é bem diferente.

Referência: Regras para dedução natural e tabelas de verdade.

Atualizado em 22/06/2006 para lógica de predicados!

Consolo para os que tem dificuldades de levantar-se nas manhãs frias do inverno (em inglês).

Visite o tree proof generator e verifique os árvores de refutação preferidos como

((\forallx(Fx\landGx\toHx)\to\existsx(Fx\land\negGx))
\land
(\forallx(Fx\toGx)\lor\forallx(Fx\toHx)))
\to
(\forallx(Fx\landHx\toGx)\to\existsx(Fx\landGx\land\negHx))

Bibliografia

Michael R. A. Huth and Mark Ryan. Logic in Computer Science. Cambridge University Press, 2nd edition, 2004. (livro texto). INF: 681.3.01 H979L2.
Dov M. Gabbay. Elementary Logics: A procedural perspective. Prentice Hall, 1998.
Krysia Broda, S. Eisenbach, H. Koshnevisan, and Steve Vickers. Reasoned Programming. Prentice Hall, 1994.
H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2nd edition, 2001. INF: 510.6 E56m.
Melvin Fitting. First-Order Logic and Automated Theorem-Proving. Springer, second edition, 1996. INF: 681.32.06 F547f2.
S. Abramsky, Dov Gabbay, and T.S.E Maibaum, editors. Handbook of Logic in Computer Science, vol I. Oxford University Press, 1992.
Jean Goubault-Larrecq and Ian Mackie. Proof Theory and Automated Deduction. Kluwer, 1997.
Graham Priest. An Introduction to Non-classical Logics. Cambridge University Press, 2001.
John Nolt and Dennis Rohatyn. Lógica. McGRaw-Hill, Makron Books, 1991.

Livro em português, com alguns exercícios suplementares. Cuida, a notação é diferente.

Mordechai Ben-Ari. Mathematical logic for computer science. Springer, second edition, 2001.

Mais sobre sistemas de lógica, inclusive os sistemas de Gentzen e Hilbert (cap. 3)

Herbert B. Enderton. A mathematical introduction to logic. Academic Press, 1792. INF: 510.6 E56m.

Mais sobre sistemas de Hilbert.

Stephen Cole Kleene. Mathematical logic. John Wiley, 1967. INF: 510.6 K63m.

Mais sobre sistemas de Hilbert.