Introducción a la Demostración Asistida por Ordenador con Isabelle/HOL

El siguiente libro gratuito está dirigido para todas aquellas personas interesadas en aprender sobre este gran tema.

El demostrador interactivo de teoremas Isabelle es una herramienta de ayuda a la demostración de teoremas escrita en el lenguaje de programación ML y desarrollada por Larry Paulson de la Universidad de Cambridge y Tobias Nipkow del Technische Universität München.

El lenguaje en que se realizan las pruebas es HOL (acrónimo de Higher-Order Logic), que es un lenguaje fuertemente tipado con estructuras de datos, funciones recursivas (incluyendo valores funcionales) y expresiones lógicas con cuantificadores.

Sobre el Libro (Por el Autor)

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.

Para 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.

hot sale domestika — Ve la oferta aquí y recuerda que tienes el 10% Extra con el código: FACIALIX-10

Contenido (Temas)

Temas
- Deducción natural en lógica proposicional
- Deducción natural en lógica de primer orden
- Resumen de Isabelle/Isar y de la lógica
- Programación funcional con Isabelle/HOL
- Razonamiento sobre programas
- Razonamiento por casos y por inducción
- Caso de estudio: Compilación de expresiones
- Conjuntos, funciones y relaciones
Ejercicios
- Deducción natural en lógica proposicional
- Argumentación lógica proposicional
- Eliminación de conectivas
- Deducción natural en lógica de primer orden
- Argumentación lógica de primer orden
- Argumentación lógica de primer orden con igualdad
- Programación funcional con Isabelle/HOL
- Razonamiento sobre programas
- Cons inverso
- Y muchos más…

Ficha Técnica

Año: 2013

Editor: Universidad de Sevilla

Idioma: Español

Tamaño: 374 KB

Licencia: CC-BY-NC-SA

Descarga el Libro

Si te interesaron los temas, te dejamos aquí abajo el enlace de descarga.

Primera Opción

Segunda Opción

Acerca de OpenLibra

OpenLibra busca reunir bajo una misma plataforma el mayor número de publicaciones libres posible. Esto implica una serie de riesgos en cuanto a los contenidos que han de asumirse y sobre los que queremos informar a nuestros usuarios.

En OpenLibra, los libros son responsabilidad exclusiva de sus autores. Esto significa que OpenLibra, no puede garantizar la validez de sus contenidos.

Preguntas Frecuentes

¿Qué quiere decir Biblioteca Libre?

Quiere decir que todos los libros que la componen están licenciados bajo alguno de los muchos tipos de licencia libre que existen y que, por tanto, el autor da su autorización para su reproducción y redistribución.

¿Son entonces todos los libros de esta biblioteca gratis?

Sí; al menos para su versión digital. Muchos autores, además, ofrecen la versión impresa (ya sea directamente o a través del circuito comercial habitual) por la que pueden cobrar lo que estimen oportuno.

Pero algunos de los libros que hay en la Biblioteca tienen Copyright…

El copyright y las licencias libres no son excluyentes. De hecho, las segundas se basan en la legislación sobre la primera para otorgar los derechos de copia y distribución. Es por eso que toda obra bajo una licencia libre, posee un copyright que garantiza la voluntad de su autor. Lo importante es qué permite ese copyright con respecto a la obra licenciada.

Cierto; en estos casos, lo más habitual es que la editorial haya devuelto los derechos de explotación al autor. Suele ocurrir con los manuales técnicos una vez pasado un tiempo prudencial o, por ejemplo, cuando se han agotado las ediciones impresas y no se pretende una reedición. Una vez los autores vuelven a tener el control, pueden ceder su trabajo al dominio público o permitir su redistribución libre para volver a poner su obra en circulación.

Si los libros son libres y gratis, ¿puedo hacer con ellos lo que quiera? ¿Los puedo imprimir, traducir y/o vender?

No; no puedes hacer aquello que su licencia no permita. Cómo se explica en el enlace de más arriba, algunas licencias solo permiten la descarga y redistribución sin ánimo de lucro. Si por ejemplo, quieres traducir la obra y editarla de forma ordinaria, algunos autores te exigirán que pagues los derechos pertinentes.