Mechanizing Mathematics

Universidad Nacional de Colombia, Sede Manizales
Facultad de Ciencias Exactas y Naturales
Classes: May, 29 (Monday) - June, 02 (Friday), 2023

General information

We are going to use the proof assistant PVS (versão 7.1) embeeded on the VS-Code software (VSCode-PVS IDE).
The instalation of PVS is not mandatory for the classes, however we encourage the participants install
the system in their machines in order to work on the exercises.

• It is possible to install VSCode-PVS from the VSCode Marketplace.
• We are going to use the NASA PVS libraries (NASALib) in some examples and exercises.
• Natively, PVS runs over Unix or MacOS plataforms (except, for now, in M1 architectures).
  In order to execute PVS over Windows or MacOS (M1 chip), it is necessary to install a virtual machine.

Program and Material

• Class 1 : 16:00 - 18:00 - May 29, 2023
• Class 2 : 16:00 - 18:00 - May 30, 2023
• Class 3 : 16:00 - 18:00 - May 31, 2023
• Class 4 : 16:00 - 18:00 - June 01, 2023
• Class 5 : 16:00 - 18:00 - June 02, 2023

Lecturers

• Mauricio Ayala-Rincón (UnB)
• Thaynara Arielly de Lima (UFG)