Razonamiento automático (2014-15)

El curso "Razonamiento automático (2014-15)" ofrece una introducción al razonamiento formal y la verificación de programas utilizando Isabelle/HOL. A lo largo del curso, se abordan temas fundamentales como la programación funcional en Isabelle, el razonamiento sobre programas (incluyendo casos de estudio como la ordenación por inserción y mezcla), la deducción natural (tanto proposicional como de primer orden), conceptos avanzados como conjuntos inductivos, gramáticas libres de contexto y razonamiento modular, así como aplicaciones prácticas como la resolución de sudokus. Además, el curso incluye una serie de relaciones de ejercicios que permiten profundizar en la formalización, automatización y verificación de propiedades en entornos de demostración asistida.

La asignatura forma parte del Máster Universitario en Lógica, Computación e Inteligencia Artificial impartido por el Departamento de Ciencias de la Computación e Inteligencia Artificial de la Universidad de Sevilla.

Temas

Ejercicios

Bibliografía

Visiones generales de la DAO

Lecturas complementarias

Programación funcional

Lógica computacional

Cursos relacionados

Cursos con Isabelle/HOL

Otros cursos

Sistemas


José A. Alonso Jiménez
Sevilla, 29 de junio del 2025
Licencia: Creative Commons.