RA2010: Razonamiento por inducción sobre los naturales
La clase de hoy del curso de Razonamiento automático ha tenido dos partes. En la primera parte se ha comentado la historia del razonamiento automático y algunos de sus logros. En la segunda parte se ha continuado la introducción de técnicas de demostración en Isabelle estudiando la demostración por inducción sobre los números naturales.
Las transparencias y apuntes usados en clase son los siguientes:
La tarea pendiente para la próxima clase consiste en escribir, y publicar en el portafolio digital, las soluciones de los ejercicios de la relación 1 y de la relación 2. Los códigos se encuentran el la página de ejercicios.