Seminarios anteriores

Sumario

Título: El papel de ACL2 para incrementar la fiabilidad de Kenzo
Ponente:
Mirian Andrés

Departamento de Matemáticas y Computación

Universidad de La Rioja
Resumen: La charla consiste en presentar de forma divulgativa una de las lineas de investigación de un grupo de la Universidad de La Rioja. Se explicarán los intereses en el uso de ACL2 y, de forma un poco más formal se mostrará, a modo de ejemplo, el trabajo Formalizing Simplicial Topology in ACL2 presentado en el pasado Workshop de ACL2 de 2007.

Título: Razonamiento conjuntista en Isabelle/Isar
Ponente: José A. Alonso
Resumen: En este seminario se presenta cómo puede razonarse con conjuntos definidos por comprensión y conjuntos finitos en Isabelle/Isar. El contenido del seminario se corresponde con el capítulo 7 de Introduccion a la demostracion asistida por ordenador (con Isabelle/Isar).

Título: Métodos formales: pasado, presente y futuro
Ponente: José A. Alonso
Resumen: En este seminario se comenta el estado actual de los métodos formales a partir de de las comunicaciones presentadas en Formal Methods Outreach Workshop (SRI Junio de 2008).

Título: Sensor-IA
Ponente: Francisco J. Martín
Resumen: Se realizará una presentación del proyecto "Sensor-IA" realizado para el Instituto Andaluz de Tecnología.

Título: Demostración en Isar de la corrección de un compilador
Ponente: José A. Alonso
Resumen: En este seminario se presenta, como caso de estudio en Isar, la demostración de la corrección de un compilador. El contenido del seminario se corresponde con el capítulo 6 de Introduccion a la demostracion asistida por ordenador (con Isabelle/Isar).

Título: Patrones de razonamiento en Isabelle/Isar
Ponente: José A. Alonso
Resumen: En este seminario se extienden los patrones de razonamiento proposicional, cuantificacional e inductivo de Isabelle/Isar. Se pondrá el énfasis en las demostraciones estructuradas. El contenido del seminario se corresponde con los capítulos 4 y 5 de Introduccion a la demostracion asistida por ordenador (con Isabelle/Isar).

Título: APLI2: pasado, presente y futuro.
Ponente: Gonzalo A. Aranda-Corral
Resumen: APLI2 es un sistema desarollado para la ayuda a la enseñanza de la Lógica. En esta charla describiremos tanto la arquitectura del sistema como usabilidad y posibles ampliaciones del sistema.

Título: Razonamiento inductivo en Isabelle/Isar
Ponente: José A. Alonso
Resumen: En este seminario se presentan los patrones de razonamiento por inducción matemática y por inducción estructural en Isabelle/Isar. El contenido del seminario se corresponde con el capítulo 3 de Introduccion a la demostracion asistida por ordenador (con Isabelle/Isar).

Título: Patrones básicos de razonamiento en Isabelle/Isar
Ponente: José A. Alonso
Resumen: En este seminario se presentan los patrones básicos de Isabelle/Isar para el razonamiento proposicional, cuantificacional y ecuacional. Se pondrá el énfasis en las demostraciones estructuradas. El contenido del seminario se corresponde con el capítulos 2 de Introduccion a la demostracion asistida por ordenador (con Isabelle/Isar).

Título: Isabelle como lenguaje de programación e Isar como lenguaje de demostración
Ponente: José A. Alonso
Resumen: Este seminario es el primero de una serie cuyo objetivo es mostrar las posibilidades de Isabelle/Isar como sistema que permite regular el nivel de automatización de las demostraciones y hacerlas legibles por los humanos y procesable por las máquinas. El contenido del seminario se corresponde con los dos primeros capítulos de Introduccion a la demostracion asistida por ordenador (con Isabelle/Isar).