15 marzo 2018 – Vestigium

LMF2017: Ejercicios de deducción natural proposicional en Isabelle/HOL

PorJosé A. Alonso 15 marzo 2018

En la clase de hoy del curso Lógica matemática y fundamentos se han comentado soluciones de ejercicios de deducción natural con Isabelle/HOL. Concretamente, los ejercicios 6, 7, 19, 28, 34, 37, 43, 44, 47 y 53 de la cuarta relación.

SLC2018: Demostraciones por inducción en Coq

PorJosé A. Alonso 15 marzo 201824 marzo 2018

En la sesión de hoy del Seminario de Lógica Computacional Alejandro Rodríguez Rodríguez ha explicado cómo demostrar en Coq propiedades de los números natuales por inducción.

La teoría, junto con los ejercicios, utilizados en la exposición son
Read More “SLC2018: Demostraciones por inducción en Coq”