4. Aula 4: Provas Regressivas
Esta aula fornece o método de prova que a Aula 3 adiou, seguindo o capítulo 3 do Hitchhiker's Guide to Logical Verification.A. Baanen, A. Bentkamp, J. Blanchette, J. Hölzl, J. Limperg, The Hitchhiker's Guide to Logical Verification, edição de 2026, capítulo 3. Ela apresenta o modo de táticas, as táticas básicas, as regras dos conectivos, dos quantificadores e da igualdade, as táticas de reescrita rw e simp e as provas por indução matemática, e reprova vários dos enunciados que a Aula 3 deixou com sorry, agora como teoremas próprios.
Esta aula também está disponível como slides de apresentação.