:!: Página descontinuada, provavelmente o material não é mais acessível.

====== Lógica para computação (2007/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.\\
**Turmas:** A,C.\\
**Horário/Sala:**\\
Turma A: Terça/Quinta, 8.30-10.10, Sala 113, [[http://www.inf.ufrgs.br/cei/nscad/images/stories/mapa_2006.jpg|prédio 43425]].\\
Turma C: Terça/Quinta, 10.30-12.10, Sala 107, [[http://www.inf.ufrgs.br/cei/nscad/images/stories/mapa_2006.jpg|prédio 43425]].\\
**Consultas:** Quarta, 15-17.\\
**Detalhes:** Vê o {{:inf05508:lpc-sy.doc|programa}}.










===== Notícias =====
  * 05/07: Notas da prova de recuperação são disponíveis. :!:

===== Resultados =====
  * [[2007-1-FF|Freqûencia]]
  * [[2007-1-Notas|Notas]]
  * [[2007-1-Trabalhos|Trabalhos]]













===== Materiais =====

  * [[http://www.inf.ufrgs.br/%7Elamb/ENSINO.html|Página da disciplina]] por [[http://www.inf.ufrgs.br/~lamb|Luís da Cunha Lamb]].
  * Página da disciplina em [[2006-2|2006/2]] e [[2006-1|2006/1]].
  * {{lpc-2251.pdf|Notas de aula}}
  * {{PR.pdf|Prova}} de recuperação com {{SPR.pdf|solução}} para preparação









==== Aulas Turma A ====

^ No.  ^ Data   ^ Tópicos                                              ^ Notas pág. ^  Exercícios  ^  Soluções 	 ^ Leitura ^
|   1  | 06/03 | Administrativa, Introdução.                           |  1-13         |  2.1-2.6    |    |  HR1.1,1.3   |
|   2  | 08/03 | Dedução natural: Regras de prova e exemplos 1.        |  13-18        |             |    |  HR1.2       |
|   3  | 13/03 | Dedução natural: Regras de prova e exemplos 2.        |  18-24        |  2.7-2.12   |    |  HR1.2       |
|   4  | 15/03 | Dedução natural: Exemplos e exercícios.               |               |             |    |  HR1.2       |
|   5  | 20/03 | Dedução natural: Leis importantes.                    |  25-30        |             |    |  HR1.2,ML§9  |
|   6  | 22/03 | Dedução natural: Exercícios.                          |               |             |    |              |
|   7  | 27/03 | Sistemas tipo Hilbert. Teoria de modelos.             |  31-35,48-52  |  2.13-2.18  |    |  HR1.4       |
|   8  | 29/03 | Indução matemática. Consistência e completude.        |  52-63        |             |    |  HR1.4       |
|   9  | 03/04 | História.                                             |  137-144      |  2.19-2.22, {{e04c.pdf|T1}}  |  {{s04c.pdf|T1}}  |  HR1.7       |
|  10  | 05/04 | Árvores de refutação. Introdução e exemplos.          |  35-48        |             |    |  NR4.4       |
|  11  | 10/04 | Exercícios: Árvores de refutação e dedução natural.   |               |  2.23,2.24  |    |              |
|  12  | 12/04 | Formas normais.                                       |  62-68        |  2.25       |    |  HR1.5       |
|  13  | 17/04 | Revisão e exercícios unidade 1.                       |               |             |    |              |
|  14  | 19/04 | **Prova 1**                                           |  {{p01b.pdf|P1}}  |         |  {{sp01b.pdf|P1}}  |  |
|  15  | 24/04 | Lógica de predicados: Introdução, exemplos.           |  81-85       |             |    |  HR2.1       |
|  16  | 26/04 | Lógica de predicados: Identidade. Exercícios de formalização. | 86-90  | 3.1,3.12  |    |  HR2.1,2.8   |
|      | 01/05 | //Feriado//: [[wppt>Dia do Trabalho]]                 |              |             |    |              |
|  17  | 03/05 | Lógica de predicados: Semântica.                      |  90-96       | 3.2,3.3     |    |  HR2.2,2.4   |
|  18  | 08/05 | Lógica de predicados: Semântica.                      |  90-96       | 3.4-3.9	    |    |  HR2.2,2.4   |
|  19  | 10/05 | Lógica de predicados: Introdução à teoria de provas.  |  97-103      |             |    |  HR2.3       |
|  20  | 15/05 | Lógica de predicados: Exemplos, exercícios.           |  97-103      | 3.9,3.10    |    |  HR2.3       |
|  21  | 17/05 | Lógica de predicados: Teoria de provas.               |      	      |    	    |    |  HR2.8       |
|  22  | 22/05 | Lógica de predicados: Teoremas.                       |  103-107     |             |    |  HR2.8       |
|  23  | 24/05 | Lógica de predicados: Árvores de refutação.           |  108-117     |    	    |    |  NR4.4       |
|  24  | 29/05 | Lógica de predicados: Árvores de refutação            |  108-177     | 3.11,3.13   |    |  NR4.4       |
|  25  | 31/05 | Lógica: Adequação e decibilidade.                     |  117-118     |    	    |    |  NS I.8-10   |
|  26  | 05/06 | Revisão unidade 2 e exercícios.                       |              |    	    |    |    	      	|
|      | 07/06 | //Feriado//: [[wppt>Corpus Cristi]]                   |              |    	    |    |    	      	|
|  27  | 12/06 | **Prova 2**                                           |  {{p02d.pdf|P2}}  |        |  {{sp02d.pdf|P2}}  |    |
|  28  | 14/06 | Apresentação de trabalhos.                            |              |    	    |    |    	      	|
|  29  | 19/06 | Apresentação de trabalhos.                            |              |    	    |    |    	      	|
|  30  | 21/06 | Visão geral, lógica de 2a ordem, complexidade.        |              |             |    |    	      	|
|      | 26/06 | Aula de revisão: Prova simulada.                      |              |             |    |    	      	|
|      | 03/07 | Prova de recuperação                                  |              |             |    |    	      	|          
| | | | | | | |
|      | 12/07 | Término oficial das aulas.  |    |    |    |    |


==== Aulas Turma C ====
^ No. ^ Data   ^ Tópicos ^ Notas pág. ^  Exercícios  ^  Soluções 	 ^ Leitura ^
|   1  | 06/03 | Administrativa, Introdução.                           |              |             |    |             	|
|   2  | 08/03 | História.                                             |              |             |    |             	|
|   3  | 13/03 | Introdução à logica proposicional.                    |  1-13        |  2.1-2.6    |    |  HR1.1,1.3  	|
|   4  | 15/03 | Dedução natural: Regras de prova e exemplos 1.        |  13-18       |             |    |  HR1.2      	|
|   5  | 20/03 | Dedução natural: Regras de prova e exemplos 2.        |  18-24       |  2.7-2.12   |    |  HR1.2      	|
|   6  | 22/03 | Dedução natural: Exemplos e exercícios.               |              |             |    |  HR1.2      	|
|   7  | 27/03 | Dedução natural: Exemplos e leis importantes.         |  25-30       |             |    |  HR1.2,ML§9 	|
|   8  | 29/03 | Sistemas de tipo Hilbert. Teoria de modelos.          |  31-35,48-52  |  2.13-2.18  |    |  HR1.4      	|
|   9  | 03/04 | Indução matemática. Consistência e completude.        |              |  2.19-2.22, {{e04c.pdf|T1}}  |  {{s04c.pdf|T1}}  |  HR1.4      	|
|  11  | 10/04 | Exercícios: Árvores de refutação e dedução natural.   |  35-48       |  2.23,2.24  |    |              |
|  12  | 12/04 | Formas normais.                                       |  62-68       |  2.25       |    |  HR1.5       |
|  13  | 17/04 | Revisão e exercícios unidade 1.                       |              |             |    |              |
|  14  | 19/04 | **Prova 1**                                           |  {{p01c.pdf|P1}}  |        |  {{sp01c.pdf|P1}}  |  |
|  15  | 24/04 | Lógica de predicados: Introdução, exemplos.           |  81-85       |  3.1        |    |  HR2.1       |
|  16  | 26/04 | Lógica de predicados: Identidade. Exercícios de formalização. | 86-90  | 3.1,3.12  |    |  HR2.1,2.8   |
|      | 01/05 | //Feriado//: [[wppt>Dia do Trabalho]]                 |              |             |    |              |
|  17  | 03/05 | Lógica de predicados: Semântica.                      |  90-96       | 3.2,3.3     |    |  HR2.2,2.4   |
|  18  | 08/05 | Lógica de predicados: Semântica.                      |  90-96       | 3.4-3.9	    |    |  HR2.2,2.4   |
|  19  | 10/05 | Lógica de predicados: Introdução à teoria de provas.  |  97-103      |             |    |  HR2.3       |
|  20  | 15/05 | Lógica de predicados: Exemplos, exercícios.           |  97-103      | 3.9,3.10    |    |  HR2.3       |
|  21  | 17/05 | Lógica de predicados: Teoria de provas.               |      	      |    	    |    |  HR2.8       |
|  22  | 22/05 | Lógica de predicados: Teoremas.                       |  103-107     |             |    |  HR2.8       |
|  23  | 24/05 | Lógica de predicados: Árvores de refutação.           |  108-117     |    	    |    |  NR4.4       |
|  24  | 29/05 | Lógica de predicados: Árvores de refutação            |  108-177     | 3.11,3.13   |    |  NR4.4       |
|  25  | 31/05 | Lógica: Adequação e decibilidade.                     |  117-118     |    	    |    |  NS I.8-10   |
|  26  | 05/06 | Revisão unidade 2 e exercícios.                       |              |    	    |    |    	      	|
|      | 07/06 | //Feriado//: [[wppt>Corpus Cristi]]                   |              |    	    |    |    	      	|
|  27  | 12/06 | **Prova 2**                                           |  {{p02c.pdf|P2}}  |        |  {{sp02c.pdf|P2}}  |    |
|  28  | 14/06 | Apresentação de trabalhos.                            |              |    	    |    |    	      	|
|  29  | 19/06 | Apresentação de trabalhos.                            |              |    	    |    |    	      	|
|  30  | 21/06 | Visão geral, lógica de 2a ordem, complexidade.        |              |             |    |    	      	|
|      | 26/06 | Aula de revisão: Prova simulada.                      |              |             |    |    	      	|
|      | 03/07 | Prova de recuperação                                  |              |             |    |    	      	|          
| | | | | | | |
|      | 12/07 | 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 os árvores de refutação preferidos como
<code>
((\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))
</code>

  * "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 ====
<html>
<!-- BEGIN BIBLIOGRAPHY livros -->
<!--
    DO NOT MODIFY THIS BIBLIOGRAPHY BY HAND!  IT IS MAINTAINED AUTOMATICALLY!
    YOUR CHANGES WILL BE LOST THE NEXT TIME IT IS UPDATED!
-->
<!-- Generated by: /home/ritt/arch/share/bin/bib2xhtml -s unsortlist livros.bib livros.html -->
<ul class="bib2xhtml">

<!-- Authors: Michael R A Huth and Mark Ryan -->
<li><a name="Huth.Ryan/2004">Michael</a> R.&nbsp;A. Huth and Mark Ryan.
<a href="http://www.cs.bham.ac.uk/research/lics"><cite>Logic in Computer
  Science</cite></a>.
Cambridge University Press, 2nd edition, 2004.
(livro texto). INF: 681.3.01 H979L2.</li>

<!-- Authors: Dov M Gabbay -->
<li><a name="Gabbay/1998">Dov</a>&nbsp;M. Gabbay.
<cite>Elementary Logics: A procedural perspective</cite>.
Prentice Hall, 1998.</li>

<!-- Authors: Krysia Broda and S Eisenbach and H Koshnevisan and Steve Vickers
  -->
<li><a name="Broda.alii/1994">Krysia</a> Broda, S.&nbsp;Eisenbach,
  H.&nbsp;Koshnevisan, and Steve Vickers.
<cite>Reasoned Programming</cite>.
Prentice Hall, 1994.</li>

<!-- Authors: H B Enderton -->
<li><a name="Enderton/2001">H</a>.&nbsp;B. Enderton.
<cite>A Mathematical Introduction to Logic</cite>.
Academic Press, 2nd edition, 2001.
INF: 510.6 E56m.</li>

<!-- Authors: Melvin Fitting -->
<li><a name="Fitting/1996">Melvin</a> Fitting.
<a href="http://comet.lehman.cuny.edu/fitting/errata/errata.html"><cite>First-Order Logic and Automated Theorem-Proving</cite></a>.
Springer, second edition, 1996.
INF: 681.32.06 F547f2.</li>

<!-- Authors: S Abramsky and Dov Gabbay and TSE Maibaum -->
<li><a name="Abramsky.alii/1992">S</a>.&nbsp;Abramsky, Dov Gabbay, and
  T.S.E Maibaum, editors.
<cite>Handbook of Logic in Computer Science, vol I</cite>.
Oxford University Press, 1992.</li>

<!-- Authors: Jean Goubault Larrecq and Ian Mackie -->
<li><a name="Goubault.Mackie/1997">Jean</a> Goubault-Larrecq and
  Ian Mackie.
<cite>Proof Theory and Automated Deduction</cite>.
Kluwer, 1997.</li>

<!-- Authors: Graham Priest -->
<li><a name="Priest/2001">Graham</a> Priest.
<a href="http://www.st-andrews.ac.uk/academic/philosophy/gp.html"><cite>An
  Introduction to Non-classical Logics</cite></a>.
Cambridge University Press, 2001.
INF:510.6 P949i.</li>

<!-- Authors: John Nolt and Dennis Rohatyn -->
<li><a name="Nolt.Rohatyn/1991">John</a> Nolt and Dennis Rohatyn.
<cite>Lógica</cite>.
McGRaw-Hill, Makron Books, 1991.</li>

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

<!-- Authors: Mordechai Ben Ari -->
<li><a name="Ben-Ari/2001">Mordechai</a> Ben-Ari.
<a href="http://stwww.weizmann.ac.il/g-cs/benari/books/index.html#ml2"><cite>Mathematical logic for computer science</cite></a>.
Springer, second edition, 2001.
INF:510.6 B456m.</li>

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

<!-- Authors: Herbert B Enderton -->
<li><a name="Enderton/1972">Herbert</a>&nbsp;B. Enderton.
<cite>A mathematical introduction to logic</cite>.
Academic Press, 1792.
INF: 510.6 E56m.</li>

 <blockquote> Mais sobre sistemas de Hilbert. </blockquote>

<!-- Authors: Stephen Cole Kleene -->
<li><a name="Kleene/1967">Stephen</a>&nbsp;Cole Kleene.
<cite>Mathematical logic</cite>.
John Wiley, 1967.
INF: 510.6 K63m.</li>

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

<!-- Authors: Anil Nerode and Richard A Shore -->
<li><a name="Nerode.Shore/2005">Anil</a> Nerode and Richard&nbsp;A.
  Shore.
<cite>Logic for applications</cite>.
Springer, second edition, 2005.</li>

<!-- Authors: H D Ebbinghaus and J Flum and W Thomas -->
<li><a name="Ebbinghaus.etal/1994">H</a>.-D. Ebbinghaus, J.&nbsp;Flum,
  and W.&nbsp;Thomas.
<cite>Mathematical logic</cite>.
Springer, 1994.
INF: 510.6 E16m.</li>

</ul>

<!-- END BIBLIOGRAPHY livros -->

</html>

<html>
<a href="http://www2.clustrmaps.com/counter/maps.php?url=http://www.inf.ufrgs.br/~mrpritt" id="clustrMapsLink"><img width=1 src="http://www2.clustrmaps.com/counter/index2.php?url=http://www.inf.ufrgs.br/~mrpritt" style="border:1px solid;" alt="Locations of visitors to this page" title="Locations of visitors to this page" id="clustrMapsImg" onError="this.onError=null; this.src='http://clustrmaps.com/images/clustrmaps-back-soon.jpg'; document.getElementById('clustrMapsLink').href='http://clustrmaps.com'" />
</a>
</html>