RA2011: Patrones de inducción en Isabelle: casos, inducción y otros

En la clase de hoy del curso de Razonamiento automático se han presentado los principales patrones de inducción en Isabelle: en la primera parte se ha presentado los patrones de de mostración por casos y por inducción y en la segunda parte se han presentado otros patrones (eliminación de disyunción, negación, contradicción y equivalencias).

La primera parte de la clase se ha basado en la siguiente teoría Isabelle
Read More “RA2011: Patrones de inducción en Isabelle: casos, inducción y otros”