Lógica Computacional 1 - 2012/1

Turma B

Turma C

Links interessantes:

  • Assistente de Prova Coq
  • Emacs
  • Emacs-mode para Coq: Proof General
  • ProofWeb
  • ProofWeb.v

    • Exercícios sobre indução matemática em Coq:

  • Soma de 1 até n: inducao1
  • Soma de quadrados de 1 até n: exercicio1
  • Soma de cubos de 1 até n : exercicio2

    • Projeto de Especificação em Coq:

  • Detalhamento do projeto
  • Relatório: relatorio.tex
  • Especificação: ordenacao.v
  • Exemplo dado em aula: arvores-binarias.v