Interactive Proof: Introduction to Isabelle/HOL
Tobias Nipkow ha publicado un nuevo tutorial de Isabell/HOL: Interactive Proof: Introduction to Isabelle/HOL, que presentará a principio de agosto en la Summer School Marktoberdorf 2011.
El contenido del tutorial es el siguiente:
- Elementos básicos de Isabelle/HOL: los tipos, términos, fórmulas y teorías.
- Isabelle/HOL como lenguaje funcional verificable. En esta sección, presenta los tipos básicos (bool, nat y list), cómo pueden definirse funciones y tipos y cómo pueden demostrarse propiedades por inducción y simplificación.
- Lógica y automatización de las demostraciones. En esta sección, presenta cómo se trabaja con fórmulas y conjuntos, cómo puede automatizarse las demostraciones de sus propiedades y cómo pueden analizarse las demostraciones en pasos elementales.
- Demostraciones estructuradas con Isar. En esta sección, presenta ejemplos de demostraciones en Isar, patrones de demostraciones, técnicas para mejorar demostraciones y demostraciones por inducción y casos en Isar.
La presentación del tutorial está basada en ejemplos: se concentra en ejemplos que presenta los casos típicos sin explicar el caso general si se puede inferir de los ejemplos.
Las teorías que sirven de ejemplo del tutorial son las siguientes: Overview, Nat, List, Tree, Simp, Induct, Auto_Proof_Demo, Single_Step_Demo, Inductive_Demo, Isar_Demo, Isar_Induct_Demo.
El resto del material utilizado se encuentra en MOD2011.