Estadísticas del PDF: Introducción a la demostración asistida por ordenador (con Isabelle/Isar)

Introducción a la demostración asistida

por ordenador (con Isabelle/Isar)

José A. Alonso Jiménez

Grupo de Lógica Computacional
Dpto. de Ciencias de la Computación e Inteligencia Artificial
Universidad de Sevilla
Sevilla, 5 de abril de 2008 (versión de 26 de mayo de 2009)

2

Índice

1

.

.

.

.

.

.

Introducción .

7
Isabelle como un lenguaje funcional
7
1.1
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2 N úmeros naturales, enteros y booleanos . . . . . . . . . . . . . . ....