Lógica para Computação

De Wiki DAINF
(Diferença entre revisões)
(Links Diversos)
(Sistemas Computacionais de Auxílio ao Aprendizado de Lógica)
Linha 105: Linha 105:
  
 
* NETO, Adolfo. '''KEMS''':  Um provador de teoremas multi-estratégia baseado no método KE. Disponível em: <http://kems.iv.fapesp.br>. Acesso em: 12 dez. 2008.
 
* NETO, Adolfo. '''KEMS''':  Um provador de teoremas multi-estratégia baseado no método KE. Disponível em: <http://kems.iv.fapesp.br>. Acesso em: 12 dez. 2008.
 +
 +
* BRODA, K.;EISENBACH, S.; KHOSHNEVISAN, H.; VICKERS, S. '''Pandora''': Proof Assistant for Natural Deduction using Organised Rectangular Areas. Disponível em: <http://www.doc.ic.ac.uk/pandora/>. Acesso em: 15 dez. 2008.
 +
** A learning support tool designed to guide the construction of natural deduction proofs.
  
 
(A FORMATAR...)
 
(A FORMATAR...)

Edição de 16h32min de 15 de dezembro de 2008

Tabela de conteúdo

Professores responsáveis

Ementa

  • Lógica Proposicional.
  • Linguagem e Semântica.
  • Sistemas Dedutivos.
  • Aspectos Computacionais.
  • O Princípio da Resolução.
  • Lógica de Predicados.
  • Substituição e Resolução.
  • Introdução ao PROLOG.
  • Aplicações em Computação: Introdução à Especificação e Verificação de Programas.

Objetivos da disciplina

Os objetivos da disciplina Lógica para Computação são "desenvolver conceitos de lógica proposicional e de predicados, prova automática de teoremas e programação em lógica".

O papel desta disciplina é o de mostrar como uma lógica pode ser vista como uma linguagem de especificação tanto de sistemas como de suas propriedades.

Sendo assim, pode-se entender a disciplina como o estudo das lógicas proposicional e predicativa do ponto de vista da verificação de propriedades por elas expressas, permitindo que o aluno seja capaz de identificar o tipo de lógica que pode ser usada para especificar um sistema ou propriedade, bem como realizar a modelagem de sistemas e propriedades por meio da lógica escolhida.

Bibliografia Básica

  • SANT'ANNA, Adonai S. O que é um Axioma. Barueri: Manole, 2003.
  • SOUZA, João N. de. Lógica para Ciência da Computação. Segunda edição. Rio de Janeiro: 2008.

Bibliografia Complementar

  • CARNIELLI, Walter A.; EPSTEIN, Richard L. Computabilidade, funções computáveis, lógica e os fundamentos da matemática. São Paulo: Editora UNESP, 2006.
  • SIPSER, Michael. Introdução à Teoria da Computação. São Paulo: Thomson Learning, 2007.
  • WITTGENSTEIN, Ludwig. Tractatus Logico-Philosophicus. São Paulo: Editora da Universidade de São Paulo, 1994.
  • CASANOVA, MARCO A.; GIORNO, F.A.C.; FURTADO, A.L. Programação em Lógica e a Linguagem Prolog. São Paulo: Edgard Blücher, 1987.
  • CLOCKSIN, W.; MELLISH, C. Programming in Prolog. Springer Verlag, 1982.
  • LLOYD, J. W. Foundations of Logic Programming. Springer Verlag, 1987.
  • CHANG, C. L.; LEE, R. C-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1987.
  • HAMILTON, A. G. Logic for Mathematicians. Cambridge University Press: 1988.
  • COSTA, Newton Carneiro Affonso da. Ensaio sobre os fundamentos da lógica. São Paulo: Hucitec, 1980.
  • HUTH, Michael; RYAN, Michael. Logic in Computer Science: modelling and reasoning about systems. Segunda edição. Cambridge University Press: 2004. 427 p.

(A FORMATAR...)

  1. Chin-Liang Chang; Richard Char-Tung Lee (1973). Symbolic Logic and Mechanical Theorem Proving, Academic Press1.
  2. Loveland, Donald W. (1978). Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6, North-Holland Publishing.
  3. Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper & Row Publishers. http://www.cis.upenn.edu/~jean/gbooks/logic.html.
  4. Duffy, David A. (1991). Principles of Automated Theorem Proving, John Wiley & Sons.
  5. Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992). Automated Reasoning: Introduction and Applications (2nd edition ed.), McGraw-Hill.
  6. Alan Robinson and Andrei Voronkov (eds.), ed. (2001). Handbook of Automated Reasoning Volume I & II, Elsevier and MIT Press.
  7. Fitting, Melvin (1996). First-Order Logic and Automated Theorem Proving (2nd edition ed.), Springer. http://comet.lehman.cuny.edu/fitting/.

Artigos

Referências

Links Diversos

Sistemas Computacionais de Auxílio ao Aprendizado de Lógica


  • NETO, Adolfo. KEMS: Um provador de teoremas multi-estratégia baseado no método KE. Disponível em: <http://kems.iv.fapesp.br>. Acesso em: 12 dez. 2008.
  • BRODA, K.;EISENBACH, S.; KHOSHNEVISAN, H.; VICKERS, S. Pandora: Proof Assistant for Natural Deduction using Organised Rectangular Areas. Disponível em: <http://www.doc.ic.ac.uk/pandora/>. Acesso em: 15 dez. 2008.
    • A learning support tool designed to guide the construction of natural deduction proofs.

(A FORMATAR...)

Ferramentas pessoais