Ferramentas de Utilizador

Ferramentas de Site


inf05508:homepage

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.

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

Notícias

  • Trabalho 1: Prazo 26 de março.

Resultados

Materiais

Aulas

No. Data Tópicos Notas pág. Exercícios Soluções Leitura
1 03/03 Administrativa, Introdução. 1-13 2.1-2.6, E01 S01 HR1.1,1.3
2 05/03 Dedução natural: Regras de prova e exemplos 1. 13-18 HR1.2
3 10/03 Dedução natural: Regras de prova e exemplos 2. 18-24 2.7-2.12 HR1.2
4 12/03 Dedução natural: Exemplos e exercícios. HR1.2
5 17/03 Dedução natural: Leis importantes. 25-30 HR1.2,ML§9
6 19/03 Sistemas tipo Hilbert. Teoria de modelos. T1
7 24/03 Indução matemática. Consistência e completude. 31-35,48-52 2.13-2.18 HR1.4
8 26/03 História. 52-63 HR1.4
9 31/03 Árvores de refutação. Introdução e exemplos. 137-144 2.19-2.22, HR1.7
10 02/04 Exercícios: Árvores de refutação e dedução natural. 35-48 NR4.4
11 07/04 Formas normais. 2.23,2.24
12 09/04 Clausulas de Horn, Resolução e Prolog 62-68 2.25 HR1.5
13 14/04 Revisão e exercícios unidade 1.
14 16/04 Prova 1 P1 SP1
21/04 Feriado: Tiradentes
15 23/04 Lógica de predicados: Introdução, exemplos. 81-85 HR2.1
16 28/04 Lógica de predicados: Identidade. Exercícios de formalização. 86-90 3.1,3.12 HR2.1,2.8
17 30/04 Lógica de predicados: Semântica. 90-96 3.2,3.3 HR2.2,2.4
18 05/05 Lógica de predicados: Semântica. 90-96 3.4-3.9 HR2.2,2.4
19 07/05 Lógica de predicados: Introdução à teoria de provas. 97-103 HR2.3
20 12/05 Lógica de predicados: Exemplos, exercícios. 97-103 3.9,3.10 HR2.3
21 14/05 Lógica de predicados: Teoria de provas. HR2.8
22 19/05 Lógica de predicados: Teoremas. 103-107 HR2.8
23 21/05 Lógica de predicados: Aula prática.
26/05 Semana acadêmica
28/05 Semana acadêmica
24 02/06 Lógica de predicados: Árvores de refutação. 108-117 T2 NR4.4
25 04/06 Lógica de predicados: Árvores de refutação. 108-177 3.11,3.13 NR4.4
26 09/06 Revisão unidade 2 e exercícios.
11/06 Feriado: Corpus Cristi
27 16/06 Prova 2 P2 SP2
28 18/06 Lógica: Adequação e decibilidade. 117-118 NS I.8-10
29 23/06 Apresentação de trabalhos.
30 25/06 Apresentação de trabalhos.
30/06 Aula de revisão: Prova simulada.
02/07 Prova de recuperação PR SPR
10/07 Término oficial das aulas.

Suplementos

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…).
((\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)

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

Locations of visitors to this page

inf05508/homepage.txt · Esta página foi modificada pela última vez em: 2010/01/18 15:45 (Edição externa)