
Introducción a la demostracción asistida por ordenador con Isabelle/HOL
José A. Alonso Jiménez
Introducción a la demostracción asistida por ordenador con Isabelle/HOL
José A. Alonso Jiménez
Book Details:
Year: | 2013 |
Publisher: | Universidad de Sevilla |
Pages: | 283 pages |
Language: | spanish |
Since: | 20/06/2016 |
Size: | 374 KB |
License: | CC-BY-NC-SA |
Content:
Este libro es una recopilación de los temas y relaciones de ejercicios del curso de Razonamiento automático. El curso es una introducción a la demostración asistida por ordenador con Isabelle/HOL y consta de tres niveles.
En el primer nivel se presenta la formalización de las demostraciones por deducción natural. La presentación se basa en la realizada en los cursos de Lógica informática (de 2º del Grado en Informática) y Lógica matemática y fundamentos (de 3º del Grado en Matemáticas), en concreto en los temas de deducción natural proposicional y de de primer orden. En este nivel se incluye los 3 primeros temas y las 6 primeras relaciones de ejercicios.
En el segundo nivel se presenta la programación funcional en Isabelle/HOL y el razonamiento sobre programas. La presentación se basa en la introducción a la programación con Haskell realizada en los cursos de Informática (de 1º del Grado en Matemáticas) y Programación declarativa (de 3º del Grado en Informática), en concreto en el tema 8 (para el razonamiento sobre programas) y en los restantes 9 primeros temas. En este nivel se incluye los temas 4, 5 y 6 y las relaciones de ejercicios desde la 7 a la 21.
En el tercer nivel se presentan casos de estudios y extensiones de la lógica para trabajar con conjuntos, relaciones y funciones. En este nivel se incluye los temas y y 8 y las relaciones de ejercicios 22 y 23.
Tanto los temas como las relaciones de ejercicios se presentan como teorías de Isabelle/HOL (versión Isabelle2013). Conforme se necesitan se va comentando los elementos del Isabelle/HOL.
Categories:
Tags:
Loading comments...
Scanning lists...
The book in numbers
rank in categories
online since
20/06/2016rate score
25votes
5Social likes
Nothing yet...Views
Downloads
Interest
Countries segmentation
Source Referers
Websites segmentation
evolution
Loading...