Interactively Proving Mathematical Theorems

Class Dates: February 11 (Tuesday) - 13 (Thursday)
Class Location: LINF, Summer Workshop on Mathematics - UnB, Brasília

Section 1 • Tuesday • February 11
Time Lecture Instructor
16:30 17:15 45 min Propositional Deduction Mauricio Ayala-Rincón
17:15 18:15 60 min Exercise Set 1 Thaynara Arielly de Lima & Mauricio Ayala-Rincón
Section 2 • Wednesday • February 12
Time Lecture Instructor
16:30 17:15 45 min Predicate Logic Thaynara Arielly de Lima
17:15 18:15 60 min Exercise Set 2 Thaynara Arielly de Lima & Mauricio Ayala-Rincón
Section 3 • Thursday • February 13
Time Lecture Instructor
14:00 14:30 30 min Induction Mauricio Ayala-Rincón
14:30 16:00 90 min Exercise Set 3 Thaynara Arielly de Lima & Mauricio Ayala-Rincón
Section 4 • Thursday • February 13
Time Lecture Instructor
16:30 16:50 20 min Ring Theory and other Algebraic PVS developments Thaynara Arielly de Lima
16:50 17:00 10 min Rewriting, Termination and Nominal developments Mauricio Ayala-Rincón
17:00 18:15 75 min Exercise Set 4 Thaynara Arielly de Lima & Mauricio Ayala-Rincón

Assistants

  • Ariane Alves Almeida
  • Tiago Mendonça Ferreira Ramos
  • Gabriel Ferreira Silva

    Additional Material

  • PVS cheatsheet