Ministério da Educação
UNIVERSIDADE TECNOLÓGICA FEDERAL DO PARANÁ
Campus Curitiba
PLANO DE ENSINO
CURSO Engenharia de Computação – Curso 212
MATRIZ
544 / 721
Regido pela Lei nº 9.394, de 20 de dezembro de 1996; pela Resolução CNE/CES n° 11,
FUNDAMENTAÇÃO
de 11 de março de 2002; e a pela Resolução CONFEA/CREA n° 1010, de 22 de agosto
LEGAL
de 2005. Aprovado pela Resolução Nº 84/06 COEPP de 17 de novembro de 2006.
DISCIPLINA/UNIDADE CURRICULAR
Lógica para Computação
CÓDIGO PERÍODO
IF61B
1º
CARGA HORÁRIA horas)
AT
AP
APS
Total
34
34
4
72
AT: Atividades Teóricas, AP: Atividades Práticas, APS: Atividades Práticas Supervisionadas.
PRÉ-REQUISITO
EQUIVALÊNCIA
Não há
OBJETIVOS
Desenvolver conceitos de lógica proposicional e predicativa, prova automática de teoremas e programação em
lógica. Mostrar como uma lógica pode ser vista como uma linguagem de especificação tanto de sistemas como
de suas propriedades. Entender as 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.
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.
CONTEÚDO PROGRAMÁTICO
ITEM
EMENTA
1
Lógica Proposicional
2
Linguagem e Semântica
3
Sistemas Dedutivos
4
Aspectos Computacionais
5
O Princípio da Resolução
6
Lógica de Predicados
7
Substituição e Resolução
8
Introdução ao PROLOG
9
Aplicações em Computação: Introdução à
Especificação e Verificação de Programas
CONTEÚDO
Introdução. A Linguagem Proposicional. Expressando Ideias com o
uso de fórmulas.
Fórmulas e subfórmulas. Tamanhos de fórmulas. Semântica.
Satisfazibilidade, Validade e Tabelas da Verdade. Consequência
lógica.
O que é um sistema dedutivo. Axiomatização. Substituições.
Axiomas, Dedução e Teoremas. O Teorema da Dedução. Introdução
à Dedução Natural. Introdução ao Método dos Tableaux Analíticos.
Correção e Completude. Decidibilidade.
Estudo sobre a implementação de um Provador de Teoremas.
Formas Normais. Forma Normal Conjuntiva ou Forma Clausal.
Forma Normal Disjuntiva.
Resolução. O Problema de Satisfazibilidade SAT.
Introdução. A Linguagem de Predicados Monádicos e Poliádicos.
Semântica. Dedução Natural. Axiomatização. Correção e
Completude. Decidibilidade e Complexidade.
Uso de Variáveis. Algoritmo de substituição. Resolução em lógica de
predicados.
Cláusulas de Horn. PROLOG. Estratégia de resolução em PROLOG.
Especificação de Programas. Programas como Transformadores de
Estados. Especificação de Propriedades sobre Programas. A Lógica
como Linguagem de Especificação. Tipos de Dados e Predicados
Predefinidos. Invariantes, Precondições e Pós-condições. Como
verificar programas. Prova de programas. Correção parcial e total de
programas. Regras e sistemas de provas.
REFERÊNCIAS
Referencias Básicas:
1. SILVA, Flávio S. C. da; FINGER, Marcelo; MELO, Ana C. V. de. Lógica para Computação. São Paulo:
Thomson Learning, 2006.
2. HUTH, Michael; RYAN, Mark. Lógica em ciência da computação: Modelagem e argumentação sobre
sistemas. 2. ed. Rio de Janeiro: LTC, 2008.
3. ALENCAR FILHO, Edgard de. Iniciação à lógica matemática. São Paulo: Nobel, 1975.
Referências Complementares:
1. FAVERO, Eloi L. Programação em Prolog: Uma abordagem prática. Universidade Federal do Pará,
2006. Disponível em: http://favero.ufpa.br/. Acesso em: 22 de fevereiro de 2011.
2. CONIGLIO, Marcelo; CARNIELLI, Walter A.; BIANCONI, Ricardo. Lógica e Aplicações (em
andamento). Disponível em: <http://www.cle.unicamp.br/prof/coniglio/LIVRO.pdf>. Acesso em: 12
dezembro 2008.
3. GALLIER, Jean H. Logic for computer science: Foundations of automatic theorem proving. 2003.
Disponível em: http://www.cis.upenn.edu/~jean/gbooks/logic.html. Acesso em: 20 fevereiro 2009.
4. BARLAND, Ian et al. Intro to logic. Disponível em: http://cnx.org/content/col10154/latest/. Acesso em:
01 outubro 2010.
5. SPIVEY, Mike. The Z notation: A reference manual. Prentice Hall International Series in Computer
Science, 1992. Disponível em: http://spivey.oriel.ox.ac.uk/~mike/zrm/. Acesso em: 24 de fevereiro de
2011.
6. BRODA, Krysia; EISENBACH, Susan; KHOSHNEVISAN, Hessam; VICKERS, Steve. Reasoned
7. programming. Prentice-Hall, 1994. Disponível em: http://www.doc.ic.ac.uk/pandora/firstyearbook.pdf.
Acesso em: 12 dezembro 2008.
8. SOUZA, João N. de. Lógica para ciência da computação: Fundamentos de linguagem, semântica e
sistemas de dedução. Rio de Janeiro: Campus, 2002.
ORIENTAÇÕES GERAIS
Sistema de Avaliação: Conforme previsto no Regulamento da Organização Didático-Pedagógica dos Cursos
de Graduação da UTFPR, capítulo VII, artigo 34, parágrafo 4º: “Considerar-se-á aprovado na disciplina, o aluno
que tiver frequência igual ou superior a 75% (setenta e cinco por cento) e Nota Final igual ou superior a 6,0
(seis), consideradas todas as avaliações previstas no Plano de Ensino”.