Lógica para Computação
De Wiki DAINF
(Diferença entre revisões)
(→Objetivos da disciplina) |
(→Em construção) |
||
| Linha 18: | Linha 18: | ||
* Sintaxe e Semântica de Lógica Proposicional | * Sintaxe e Semântica de Lógica Proposicional | ||
| − | *Sintaxe de Lógica de Predicados | + | * Sintaxe de Lógica de Predicados |
| − | * | + | * Algum método de demosntração para Lógica Proposicional (TAbv |
**(os três itens acima são assuntos da prova 1 - serão cobrados indiretamente) | **(os três itens acima são assuntos da prova 1 - serão cobrados indiretamente) | ||
Edição de 13h47min de 16 de setembro de 2011
Tabela de conteúdo |
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
- Algum método de demosntração para Lógica Proposicional (TAbv
- (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?
- Adquirir conhecimentos para trabalhar em empresas como:
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.
- 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/
- Tradução de:
- 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.
