Introducción a la demostracción asistida por ordenador con Isabelle/HOL

Introducción a la demostracción asistida por ordenador con Isabelle/HOL

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.

Añadir nuevo comentario