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

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: B.
Horário/Sala: Terça/Quinta 15.30-17.10, Sala 113, prédio 43425.
Consultas: TBD.
Detalhes: Vê o programa.

• Trabalho 1: Prazo 26 de março.

• Freqüência
• Notas
• Trabalhos

• Página da disciplina em 2008/2, 2008/1, 2007/2, 2007/1, 2006/2 e 2006/1.
• Notas de aula (atualizado 14/05/2009)

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

• Use um applet para resolver problemas na lógica propositional (um outro, tem milhões…).

• Visite o tree proof generator e verifique as árvores de refutação preferidas 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))

ou

(\forallx\existsy Rxy\land(\forallx\forally\forallz (Rxy\land Ryz\to Rxz)))\to\existsx Rxx

• ProofWeb é um sistema de prova online, que permite a construção de provas com dedução natural do tipo Gentzen.

• “Logic is invincible because in order to combat logic it is necessary to use logic.” (Pierre Boutroux)

• LÓGICA, s. Arte de pensar e argumentar em estrita concordância com as limitações e incapacidades da incompreensão humana. A base da lógica é o silogismo, que consiste numa premissa maior, outra menor e numa conclusão. Por exemplo:
  

Premissa maior: Sessenta homens podem executar um trabalho sessenta vezes mais rápido do que um homem só.
Premissa menor: Um homem pode cavar um buraco em sessenta segundos.
Conclusão: Logo, sessenta homems podem cavar um buraco em um segundo.
Esta pode ser chamado de silogismo aritmético, por meio do qual, combinando lógica e matemática, obtemos uma dupla certeza e somos duplamente abençoados.
(Ambrose Bierce, O dicionário do diabo)

• 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. INF:510.6 P949i.
• 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. INF:510.6 B456m.

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.

Introdução clássica. (Sobre sistemas de Hilbert: paragraph 9 ff.)

• Anil Nerode and Richard A. Shore. Logic for applications. Springer, second edition, 2005.
• H.-D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical logic. Springer, 1994. INF: 510.6 E16m.