|
Razonamiento Automático (2021-22) |
|
| Temas |
| Ejercicios |
| Sistemas |
| Documentación |
| Trabajos |
| Entrar |
Bloque 0: Introducción
| Tema 01: | Introducción al Razonamiento Automático |
| Tema 02: | Lógicas clásicas |
Bloque 1: Resolución (Otter)
| Tema 03: | Otter: Introducción |
| Ejemplos: fichas.in, grupos.in, circuitos.in | |
| Tema 04: | Otter: Resolución en lógica de primer orden |
| Ejemplos: ejemplo.in, argumentacion-1a.in, argumentacion-1b.in, argumentacion-1c.in, argumentacion-1d.in, argumentacion.in, factorizacion.in, tautologias.in, respuestas-1.in, respuestas-2.in, respuestas-3.in, respuestas-4.in, respuestas-5.in | |
| Tema 05: | Otter: Tratamiento de la igualdad |
| Ejemplos: francisco.in, opuesta.in, mayor.in, paramodulacion.in, casados.in, grupo.in | |
| Tema 06: | Otter: Predicados evaluables |
| Ejemplos: jarras.in |
Bloque 2: Inducción (Isabelle)
| Tema 07: | Isabelle: Introducción |
| Programación Funcional en Isabelle | |
| Tema 08: | Isabelle: Recursión e Inducción |
| Recursión e Inducción en Isabelle | |
| Tema 09: | Isabelle: Simplificación por reescritura |
| Razonamiento Ecuacional en Isabelle (Actualizado) |
Bloque 3: Deducción natural (LEAN)
| Tema 10: | Deducción natural proposicional |
| Lógica proposicional con LEAN | |
| Vídeo 1, Vídeo 2, Vídeo 3, Vídeo 4, Víedo 5. | |
| Tema 11: | Deducción natural en lógica de primer orden |
| Lógica de primer orden con LEAN | |
| Vídeo 1. | |
| Tema 12: | Conjuntos con LEAN: Vídeo 1. |
| Relaciones con LEAN | |
| Funciones con LEAN | |
| Números naturales, recursión e inducción con LEAN | |
| Razonamientos sobre programas |