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

Bem-vindo à lógica.

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.

• 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.

• Perigo de FF
• Notas
• Trabalhos

• 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.

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

• 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))

• 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.