Razonamiento automático (2002-03)
El curso se organiza en dos partes. En la primera, se exploran los fundamentos del razonamiento automático utilizando los sistemas Otter y Mace, además de desarrollarse algunas aplicaciones prácticas con ellas. En la segunda parte, usando Prolog, se construyen sistemas de razonamiento mediante los métodos de tableros semánticos y de resolución.
Temas
- Tema 1: Introducción a la deducción automática.
- Tema 2: Cálculo semántico proposicional con MACE.
- Tema 3: Procedimiento general de demostración por resolución proposicional en OTTER.
- Tema 4: Resolución de primer orden.
- Tema 5: Razonamiento automático con igualdad.
- Tema 6: Aplicaciones de razonamiento automático.
- Tema 7: Formalización en Prolog de la lógica proposicional.
- Tema 8: Implementación en Prolog de los tableros semánticos.
- Tema 9: Implementación en Prolog de la transformación a cláusulas.
- Tema 10: Implementación en Prolog de la resolución.