1. Aula 1: Motivação e Lógica Proposicional🔗

Esta aula motiva a verificação formal de software e revisa a lógica proposicional, seguindo o capítulo 1 de How To Prove It with Lean (HTPIwL). Ela apresenta os conectivos, as equivalências clássicas, as regras de dedução natural, a sua codificação em Lean como termos de prova e as provas com táticas.

Esta aula também está disponível como slides de apresentação.

1. 1.1. Por que Verificar Software Formalmente?
2. 1.2. Proposições
3. 1.3. Conectivos
4. 1.4. Equivalência Lógica
5. 1.5. Dedução Natural
6. 1.6. A Sintaxe de Lean
7. 1.7. Dedução Natural em Lean
8. 1.8. Provando com Táticas
9. 1.9. Exemplos Resolvidos
10. 1.10. Exercícios