Lógica para Computação

Informações Gerais

• Professores responsáveis
• Oferecimentos, dados de aprovação e alunos-destaque
• Ementa e pré-requisitos

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.

Em construção

Ao final da disciplina o aluno deverá será capaz de:

• Sintaxe e Semântica de Lógica Proposicional
• Sintaxe de Lógica de Predicados
• KE para Lógica Proposicional
  • (os três itens acima são assuntos da prova 1 - serão cobrados indiretamente)

• KE para Lógica de Predicados
  • saber fazer demonstrações de sequentes da lógica de predicados usando o sistema KE

• Substituição/Unificação (ver Apostila)
  • conceitos (substituição, unificação, unificador mais geral, etc.)
  • saber executar o Algoritmo de Unificação

• Semântica de Lógica de Predicados (Cap.2 HuthRyan)
  • conceitos (modelo, tabela/contexto, etc.)
  • saber construir um modelo para uma fórmula/sequente
  • saber demonstrar se um modelo satisfaz/falsifica/valida uma fórmula/sequente

• Formas Normais (Cap.3 de SFM06):
  • saber obter a forma normal conjuntiva/disjuntiva de uma fórmula, justificando cada passo.
  • conceitos

Prolog (livro do Eloi Favero):

• • Saber qual vai ser a resposta do Prolog a determinadas consultas (com uso, inclusive, de assert e retract) (ex.: mini-prova 2 do BSI)
  • Saber escrever programinhas do nível de complexidade dos vistos em sala de aula (ex.: questões genealógicas) exceto Torre de Hanoi
  • conceitos

• Especificação Formal (Cap.6 de SFM06):

• • Saber escrever uma especificação de uma operação (ex. Copa dp Brasil, Jogo da Velha, Ordenações de Vetores)
  • conceitos

• Verificação Formal (Cap.6 de SFM06):

• • ideia geral de todos os conceitos (sistema, regras, correção, completude, etc).
  • Correção Parcial
  • Até antes de While Parcial
  • saber escrever uma demonstração em formato de tabela
  • While Parcial
  • (NÃO) saber escrever uma demonstração em formato de tabela
  • saber ver uma demonstração em formato de tabela e dizer se ela está correta ou não
  • Correção Total
  • While Total
  • (NÃO) saber ver uma demonstração em formato de tabela e dizer se ela está correta ou não
  • NÃO exigirei que saiba escrever uma demonstração

Porque estudar lógica?

• Why Logic is Important for Computer Science and Mathematics
• Why Study Formal Logic?

• Por que precisamos ensinar lógica e como devemos ensiná-la?, Mária Bakó
  • Why we need to teach logic and how can we teach it?, Mária Bakó

• Adquirir conhecimentos para trabalhar em empresas como:
  • http://www.grupo-aes.com.br/site/home/

Bibliografia Básica

• SILVA, Flávio S. C. da; FINGER, Marcelo; MELO, Ana C. V. de. Lógica para Computação. São Paulo: Thomson Learning, 2006.
  • Este livro conquistou o primeiro lugar do Prêmio Jabuti 2007 na categoria Ciência Exatas, Tecnologia e Informática.
  • Respostas dos Exercícios do livro "Lógica para Computação"

• HUTH, Michael; RYAN, Mark. Lógica em Ciência da Computação: modelagem e argumentação sobre sistemas. Segunda edição. Editora LTC: 2008. 326 p.
  • Tradução de:
    • HUTH, Michael; RYAN, Mark. Logic in Computer Science: modelling and reasoning about systems. Segunda edição. Cambridge University Press: 2004. 427 p.
    • Página do livro original (contém errata): http://www.cs.bham.ac.uk/research/projects/lics/

• SOUZA, João N. de. Lógica para Ciência da Computação. Segunda edição. Rio de Janeiro: 2008.
  • Leia resenha bastante crítica de Walter Carnielli sobre a primeira edição deste livro publicada na revista Espiral: http://www.eca.usp.br/njr/espiral/noosfera18b.htm. Leia também, de Carnielli e Coniglio, uma crítica mais detalhada: A lógica e o consortio daemoniorum. Disponível em: <ftp://ftp.cle.unicamp.br/pub/arquivos/educacional/consortio-daemoniorum.pdf>. Acesso em: 09 dez. 2008.