MAC 239 - Métodos Formais em Programação

Segundo semestre de 2004

 
 

• 25 de agosto:
  • Introdução, histórico.
  • Monty Python: provar que alguém é uma bruxa
  • Sistemas formais: MU-puzzle ("Gödel, Escher and Bach", Douglas Hofstadter)
  • Linguagem da lógica proposicional, fórmulas bem formadas (seções 1.1 e 1.3 do livro)


• 27 de agosto:
  • Fórmulas bem formadas, árvore de análise
  • Dedução natural (seção 1.2 do livro):
    • Introdução e eliminação da conjunção
    • Introdução e eliminação da dupla negação
    • Eliminação da implicação - Modus Ponens e Modus Tollens


• 1 de setembro:
  Dedução natural (seção 1.2 do livro):
  • Introdução da implicação (suposições)
  • Introdução e eliminação da disjunção
  • Teoremas e contradições
  • Eliminação da contradição
  • Introdução e eliminação da negação


• 3 de setembro: Aula de exercícios
  • Feitos em aula:
    • Ex 1.4: 1b, 2a, 2e, 2o, 2q
    • Ex 1.5: 1d, 1e, 1f
    • Ex 1.6: 2e, 3c
  • Lista (data de entrega:15/9)


• 8 de setembro:
  • Dedução natural (seção 1.2 do livro):
    • Regras derivadas: MT, RAA e LEM
    • Resumo
  • Semântica da lógica proposicional (seção 1.4):
    • Tabelas-verdade
    • Valorações
    • Consequência lógica


• 10 de setembro: (seção 1.4)
  • Consequência lógica
  • Tautologias
  • Correção da dedução natural


• 15 de setembro: (seção 1.4)
  • Indução na estrutura de fórmulas
  • Teorema da completude


• 17 de setembro: (seção 1.5)
  • Equivalência semântica
  • Forma normal conjuntiva (CNF)
  • Validade e satisfazibilidade de fórmulas em CNF


• 22 de setembro: Aula de exercícios
  • Feitos em aula:
    • Ex 1.8: 1, 5
    • Ex 1.10: 2b e 2c
    • Ex 1.11: 2a e 2b
    Ex 1.12: 3 (só a prova para {-> e contradição})
  • Lista (data de entrega: 8/10)


• 24 de setembro: Lógica de primeira ordem.
  • Necessidade de linguagem mais rica (seção 2.1)
  • Definição da linguagem: termos e fórmulas (seção 2.2)


• 29 de setembro: Não haverá aula
• 1 de outubro: Não haverá aula


• 6 de outubro:
  • Variáveis livres (seção 2.2)
  • Substituições (seção 2.2)
  • Dedução Natural: introdução e eliminação da igualdade (seção 2.3)


• 8 de outubro: Dedução Natural: Introdução e eliminação dos quantificadores (seção 2.3)


• 13 de outubro:
  • Equivalências entre fórmulas com quantificadores (seção 2.3)
  • Forma prenex


• 15 de outubro: Aula de exercícios
  • Feitos em aula:
    • Ex 2.1: 2, 5
    • Ex 2.3: 2
    • Ex 2.5: 1e, 7f, 8a, 9a
  • Lista (data de entrega: 27/10)


• 20 de outubro: P1
  


• 22 de outubro:
  • Correção da prova
  • Semântica da lógica de predicados: modelos (seção 2.4.1)


• 27 de outubro: Semântica da lógica de predicados:
  • Interpretação de termos
  • Avaliação de fórmulas em modelos
  • Conseqüência semântica (seção 2.4.2)


• 29 de outubro: (seção 2.5)
  • Problema da correspondência de Post
  • Indecidibilidade da lógica de primeira ordem


• 3 de novembro: Aula de exercícios
  • Feitos em aula:
    • Ex 2.6: 1, 5a
    • Ex 2.7: 1a, 4, 6a, 6d, 8a
    • Ex 2.8: 1b, 2b, 2c
  • Lista (data de entrega: 24/11)


• 5 de novembro: Verificação formal de programas (seção 4.2)
  • Linguagem para descrição dos programas
  • Triplas de Hoare
  • Correção parcial e total
  • Uso de variáveis lógicas na especificação


• 10 de novembro: Correção parcial (seção 4.3)
  • Regras do cálculo de correção parcial
  • Notação alternativa (tableaux)
  • Uso das regras de implicação, atribuição e if


• 12 de novembro: Correção parcial (seção 4.3)
  • Invariantes
  • Uso da regra do while


• 17-19 de novembro: Não haverá aula


• 24 de novembro:
  • Problema do segmento de soma mínima
  • Correção total (seção 4.4)


• 26 de novembro: Aula de exercícios. Lista (data de entrega: 3/12)


• 1 de dezembro:
  • Introdução à lógica modal
  • O problema dos sábios e seus chapéus
  
  
  • 3 de dezembro
  
  
  • 8 de dezembro: P2