En la clase de hoy del curso de Demostración asistida por ordenador (DAO2011) se ha estudiado cómo demostrar con Isabelle propiedades de programas funcionales.
La teoría correspondiente a la clase es Tema_2.thy cuyo contenido se muestra a continuación
Read More “DAO2011: Razonamiento sobre programas con Isabelle”
En la clase de hoy del curso de Demostración asistida por ordenador (DAO2011) se ha presentado Isabelle como un sistema de programación funcional que permite
La teoría correspondiente a la clase es Tema_1.thy cuyo contenido se muestra a continuación
Read More “DAO2011: Isabelle como un lenguaje funcional”
En la clase de hoy del curso de Demostración asistida por ordenador (DAO2011) se ha realizado una presentación del razonamiento automático mostrando ejemplos de razonamiento asistido por los siguientes sistemas: Prover9, ACL2, PVS e Isabelle. Además, se ha comentado las principales aplicaciones desarrolladas en cada uno de ellos.
Las transparencias utilizadas, con los correspondientes enlaces, son las que se muestran a continuación:
Read More “DAO2011: Panorama del razonamiento automático a través de Prover9, ACL2, PVS e Isabelle”
Demostración asistida por ordenador (DAO2011) es un curso de formación especializada del Centro de Formación Permanente de la Universidad de Sevilla que se impartirá desde el 24 de febrero al 24 de junio de 2011.
Este curso es una introducción a la demostración asistida por ordenador usando el sistema Isabelle/HOL/Isar). Los objetivos del curso son:
Para más información se puede consultar la página del curso