LMF2019: Razonamiento por casos y por inducción en Isabelle/HOL
En la clase de hoy del curso de Razonamiento automático hemos profundizado en el estudio de las demostraciones por casos y por inducción. En concreto, se ha estudiado
- el razonamiento por casos booleanos,
- el razonamiento por casos booleanos sobre una variable,
- el razonamiento por casos sobre listas,
- el razonamiento por inducción sobre números naturales con patrones,
- el razonamiento sobre definiciones con existenciales,
- el uso de librerías auxiliares (como Parity) y
- el uso de otros métodos de demostración (como presburg).
La clase se ha dado mediante videoconferencia y el vídeo correspondiente es:
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2019: Razonamiento por casos y por inducción en Isabelle/HOL”