LogoUTFPR

Ministério da Educação

Universidade Tecnológica Federal do Paraná

Campus Curitiba         

 

 

 

 

 

 

 

 

 

 


 

LÓGICA PARA COMPUTAÇÃO (IF61B)

 


 

 

 

  1. Ementa
  2. Conteúdo Programático
  3. Objetivos da disciplina
  4. Referências
  5. Notas de aula
  6. Outros Recursos
  7. Avaliação de Aprendizagem
  8. Professor Responsável

 

 


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:

 

Un

Item da ementa

Conteúdo

0

Introdução.

O que é Lógica? Lógica Aristotélica.

1

Lógica Proposicional.

Introdução. A Linguagem Proposicional.  Expressando Idéias com o uso de fórmulas.

2

Linguagem e Semântica.

Fórmulas e subfórmulas. Tamanho de fórmulas. Semântica. Satisfabilidade e Validade. Tabelas da Verdade. Consequência e equivalência lógica.

3

Sistemas Dedutivos.

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.

4

Aspectos Computacionais.

Estudo sobre a implementação de um Provador de Teoremas. Formas Normais. Forma Normal Conjuntiva ou Forma Clausal. Forma Normal Disjuntiva.

5

O Princípio da Resolução.

Resolução. O Problema de Satisfabilidade SAT.

6

Lógica de Predicados.

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.

7

Substituição e Resolução.

Uso de Variáveis.  Algoritmo de substituição. Resolução em lógica de predicados.

8

Introdução ao PROLOG.

Cláusulas de Horn. PROLOG. Estratégia de resolução em PROLOG.

9

Introdução à Especificação e Verificação de Programas.

Especificação de Programas. Programas como Transformadores de Estados. Especificação de Propriedades sobre Programas. A Lógica como Linguagem de Especificação. Invariantes, Precondições e Pós-condições. Prova de programas. Correção parcial e total 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.

 


Referências:

 

1.       LÓGICA PARA COMPUTAÇÃO. Flávio Soares Corrêa da Silva, Marcelo Finger e Ana Cristina Vieira de Melo. Thomson Pioneira Editora, ISBN: 8522105170, 244 p., 2006.

2.       LÓGICA EM CIÊNCIA DA COMPUTAÇÃO. Michael Huth e Mark Ryan. LTC – Livros Técnicos e Científicos Editora, ISBN: 9788521616108, 322 p., 2008.

3.       PROGRAMACAO EM LOGICA E A LINGUAGEM PROLOG. Marco A. Casanova, F.A.C. Giorno, A.L. Furtado. E. Blucher, 1 ª ed., 1987.

4.       LÓGICA PARA CIÊNCIA DA COMPUTAÇÃO. João Nunes de Souza. Editora Campus. ISBN: 8535210938, 317 p., 2002.

5.       PROGRAMMING IN PROLOG. W. Clocksin, C. Mellish. Springer Verlag, 1982.

6.       FOUNDATIONS OF LOGIC PROGRAMMING. J.W. Lloyd. Springer Verlag, 1987.

7.       SYMBOLIC LOGIC AND MECHANICAL THEOREM PROVING. C-L. Chang, R. C-T. Lee. Academic Press, 1987.

8.       LOGIC FOR MATHEMATICIANS. A.G. Hamilton. Press; 2 ª ed., ISBN: 0521368650, 236 p., 1988.

 


Notas de Aula:

 

(Arquivos pdf conforme o andamento da disciplina, em constante atualização).

 

  1. Introdução
  2. Lógica Proposicional
  3. Sistemas Dedutivos
  4. Algoritmo de Wang e Resolução
  5. Lógica Predicativa
  6. Resolução e PROLOG
  7. Especificação e Verificação de Programas

 


 

EXERCÍCIOS SELECIONADOS do livro LÓGICA PARA COMPUTAÇÃO. Flávio S. C. da Silva, Marcelo Finger e Ana C. V. de Melo:

·         1.1, 1.2, 1.3, 1.6 pgs. 12 e 13;

·         1.7, 1.8 pg. 16;

·         1.9, 1.10, 1.12 pgs. 20 e 21;

·         1.14, 1.15, 1.16, 1.18, 1.20, 1.21 pgs. 27 e 28;

·         2.2, 2.3 pg. 40;

·         2.6, 2.7 pgs. 47 e 48;

·         2.10, 2.11 pgs. 55 e 56.

 


Monitoria: Acadêmico João Pedro Costa Miranda (Horário disponível no DAINF).

 

·         1ª. LISTA DE EXERCÍCIOS

·         2ª. LISTA DE EXERCÍCIOS

·         3ª. LISTA DE EXERCÍCIOS

·         4ª. LISTA DE EXERCÍCIOS

·         5ª. LISTA DE EXERCÍCIOS

·         6ª. LISTA DE EXERCÍCIOS

 


Outros recursos:

 

1.       Prática em tabelas-verdade: http://en.wikipedia.org/wiki/Truth_table; http://www.brian-borowski.com/Software/Truth/ (OBSERVAÇÃO: neste software o conectivo implica (=>) é aninhado à esquerda, diferentemente do convencionado no livro texto e adotado em nossa matéria; logo deve-se incluir parênteses quando necessário);

2.       Sistema para provas por dedução natural: JAPE http://www.cs.ox.ac.uk/people/bernard.sufrin/jape.html;

3.       Algumas provas de conjecturas em JAPE: http://www.dainf.ct.utfpr.edu.br/~kaestner/Logica/Provas26-05-2014.jp;

4.       Tabela de regras de inferência para dedução natural: http://www.dainf.ct.utfpr.edu.br/~kaestner/Logica/RegrasInferenciadaDeducaoNatural.pdf.

5.       Site com provador para Dedução Natural: http://teachinglogic.liglab.fr/DN/index.php.

6.       Site com provador em Applet Java baseado em tableaux semânticos: www.umsu.de/logik/trees;

7.       Método dos tableaux analíticos em LISP: http://www.dainf.cefetpr.br/~kaestner/Logica/tableau-method.lsp;

8.       Algoritmo de Wang em LISP: http://www.cse.buffalo.edu/~shapiro/Reasoning/wang.html;

9.       Procedimento de Resolução em LISP: http://www.dainf.cefetpr.br/~kaestner/Logica/resolution-method.lsp;

10.   Como usar os algoritmos de Wang, tableaux analíticos, resolução em LISP: HTTP://www.dainf.ct.utfpr.edu.br/~kaestner/Logica/HowtoLisp.txt;

11.   Curso “Foundations of Logic and Inference” de Stuart C. Shapiro: http://www.cse.buffalo.edu/~shapiro/Reasoning/;

12.   Livro “Logic for Computer Science” de Steve Reeves e Mike Clarke: http://www.cs.waikato.ac.nz/~stever/LCS.pdf;

13.    Cursos de PROLOG: https://www.csupomona.edu/~jrfisher/www/prolog_tutorial/contents.html e http://www.doc.gold.ac.uk/~mas02gw/prolog_tutorial/prologpages/;

14.    Interpretador PROLOG: http://www.swi-prolog.org/;

15.  Linguagem LISP: http://clisp.cons.org/ e http://www.franz.com/downloads/clp/survey.

 


Avaliação de aprendizagem:

Será constituída de provas escritas e listas de exercícios conforme indicado em sala de aula. Considerando notas N1, N2 e N3 será considerado aprovado o aluno que obtiver e (N1+N2+N3) / 3  >= 6,0. No outro caso o aluno deverá realizar uma verificação complementar (prova de recuperação R, que versará sobre todo o conteúdo do semestre), e será considerado aprovado se obtiver (N1+N2+N3+ 3*R) / 6 >= 6,0. Em ambos os casos o aluno deve ter frequência mínima às aulas conforme a legislação vigente. OBSERVAÇÃO: No caso de não comparecimento justificado a uma das provas, a nota da prova de recuperação será usada para substituí-la.

 

DATAS DAS PROVAS:

·         1ª. Verificação de aprendizagem:          13 de novembro de 2014

·         2ª. Verificação de aprendizagem:          09 de dezembro de 2014

·         3ª. Verificação de aprendizagem:          26 de fevereiro de 2015

·         Verificação complementar:                      03 de março de 2015

 

PROVAS ANTERIORES (consulte)

RESPONSABILIDADE ÉTICA ACADÊMICA: A utilização de recursos ilícitos na resolução das provas (cola) e / ou plágio em trabalhos, etc. implica na atribuição da nota 0,0 (zero) ao conceito correspondente, e a tomada das providencias administrativas cabíveis, de acordo com a política da Instituição.

RESULTADO DAS AVALIAÇÕES 2. Semestre 2014 (TURMA S01) (TURMA S71)


 

Professor Responsável:

 

Celso Antônio Alves Kaestner, Dr. Eng. Elétrica