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 e as primeiras provas estruturadas em Lean.

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. Primeiras Provas em Lean
6. 1.6. Exercícios