====== Lógica para computação (2008/2) ======
//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, [[http://www.inf.ufrgs.br/cei/nscad/images/stories/mapa_2006.jpg|prédio 43425]].\\
**Consultas:** TBD.\\
**Detalhes:** Vê o {{:inf05508:lpc-sy.doc|programa}}.
===== Notícias =====
* Primeira aula: dia 05 de agosto.
* :!: Temos um **monitor**, o [[http://www.inf.ufrgs.br/~gkaraujo/monitoria.html|Guilherme Krüger Araújo]], para a disciplina de lógica! Ele está disponível na sala da monitoria (106) para responder questões e ajudar resolver exercícios.
* Uma {{p01a.pdf|prova antiga}} com {{sp01a.pdf|soluções}} para preparação.
===== Resultados =====
* [[2008-2-FF|Freqüência]]
* [[2008-2-Notas|Notas]]
* [[2008-2-Trabalhos|Trabalhos]]
===== Materiais =====
* Página da disciplina em [[2008-1|2008/1]], [[2007-2|2007/2]], [[2007-1|2007/1]], [[2006-2|2006/2]] e [[2006-1|2006/1]].
* {{lpc-notas-2680.pdf|Notas de aula}} (atualizado 03/06/2008)
===== Aulas =====
^ No. ^ Data ^ Tópicos ^ Notas pág. ^ Exercícios ^ Soluções ^ Leitura ^
| 1 | 05/08 | Administrativa, Introdução. | 1-16 | 7.1-7.6, {{e01.pdf|E1}} | {{s01.pdf|S1}} | HR1.1,1.3 |
| 2 | 07/08 | Dedução natural: Regras de prova e exemplos 1. | 17-23 | | | HR1.2 |
| 3 | 12/08 | Dedução natural: Regras de prova e exemplos 2. | 23-30 | 7.7-7.14 | | HR1.2 |
| 4 | 14/08 | Dedução natural: Exemplos e exercícios. | | | | HR1.2 |
| 5 | 19/08 | Dedução natural: Leis importantes. | 30-35 | | | HR1.2,ML§9 |
| 6 | 21/08 | Sistemas tipo Hilbert. Teoria de modelos. | 35-38,47-54 | 7.15-7.18,7.26 | | HR1.4 |
| 7 | 26/08 | Consistência e completude. | 55-62 | 7.19-7.20 | | HR1.4 |
| 8 | 28/08 | Árvores de refutação. Introdução e exemplos. | 38-46 | | | NR4.4 |
| | 02/09 | //Sem aula// | | | | |
| | 04/09 | //Sem aula// | | | | |
| 9 | 09/09 | Exercícios: Árvores de refutação e dedução natural. | | {{e06.pdf|E2}} | {{s06.pdf|S2}} | |
| 10 | 11/09 | Formas normais. Decibilidade. | 62-67 | 7.28, {{e04f.pdf|T1}} | {{s04f.pdf|ST1}} | HR1.5 |
| 11 | 16/09 | Clausulas de Horn, Resolução e Prolog. | 69-80 | | | |
| 12 | 18/09 | História. | 185-191 | | | HR1.7 |
| 13 | 23/09 | Revisão e exercícios unidade 1. | | 7.21-7.24 | | |
| 14 | 25/09 | **Prova 1** | | {{p01g.pdf|P1}} | {{sp01g.pdf|SP1}} | |
| 15 | 30/09 | Lógica de predicados: Introdução, exemplos. | 93-97 | | | HR2.1 |
| 16 | 02/10 | Lógica de predicados: Identidade. Exercícios de formalização. | 97-103 | 14.1,14.12 | | HR2.1,2.8 |
| 17 | 07/10 | Lógica de predicados: Semântica. | 105-111 | 14.2,14.3 | | HR2.2,2.4 |
| 18 | 09/10 | Lógica de predicados: Semântica. | 105-111 | 14.4-14.9 | | HR2.2,2.4 |
| 19 | 14/10 | Lógica de predicados: Introdução à teoria de provas. | 113-123 | | | HR2.3 |
| 20 | 16/10 | Lógica de predicados: Exemplos, exercícios. | 113-123 | 14.9,14.10 | | HR2.3 |
| | 21/10 | //[[http://semac.inf.ufrgs.br|Semana academica]]// | | | | |
| | 23/10 | //[[http://semac.inf.ufrgs.br|Semana academica]]// | | | | |
| | 28/10 | //Sem aula// | | {{e07.pdf|T2}} | {{s07.pdf|ST2}} | |
| | 30/10 | //Sem aula// | | | | |
| 21 | 04/11 | Lógica de predicados: Teoria de provas. | | | | HR2.8 |
| 22 | 06/11 | Lógica de predicados: adequação e decibilidade. | 135-138 | | | NS I.8-10 |
| 23 | 11/11 | Lógica de predicados: Árvores de refutação. | 124-134 | | | NR4.4 |
| 24 | 13/11 | Lógica de predicados: Árvores de refutação | 124-134 | 14.12,14.14,14.15 | | NR4.4 |
| 25 | 18/11 | Visão geral, lógica de 2a ordem, complexidade. | | | | |
| 26 | 20/11 | Revisão unidade 2 e exercícios. | | | | |
| 27 | 25/11 | **Prova 2** | | {{p02g.pdf|P2}} | {{sp02g.pdf|SP2}} | |
| 28 | 27/11 | Tópicos. | | | | |
| 29 | 02/12 | Apresentação de trabalhos. | | | | |
| 30 | 04/12 | Apresentação de trabalhos. | | | | |
| | 09/12 | Prova de recuperação | | {{prg.pdf|PR}} | {{sprg.pdf|SPR}} | |
| | | | | | | |
| | 09/12 | Término oficial das aulas. | | | | |
===== Suplementos =====
* {{:lpc-boole-investigation.pdf|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 [[http://www.oursland.net/aima/propositionApplet.html|um applet]] para resolver problemas na lógica propositional (um [[http://www.brian-borowski.com/Truth|outro]], tem milhões...).
* Visite o [[http://www.umsu.de/logik/trees|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
* [[http://prover.cs.ru.nl/login.php|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." ([[wp>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.\\
([[wp>Ambrose Bierce]], O dicionário do diabo)
===== Bibliografia =====
Livro em português, com alguns exercícios suplementares. Cuida, a notação é diferente.
Mais sobre sistemas de lógica, inclusive os sistemas de Gentzen e Hilbert (cap. 3)
Mais sobre sistemas de Hilbert.
Introdução clássica. (Sobre sistemas de Hilbert: paragraph 9 ff.)