|
|
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-1.in,
argumentacion-1a.in,
argumentacion-1b.in,
argumentacion-1c.in,
argumentacion-1d.in,
argumentacion-1.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 (ACL2)
Bloque 3: Deducción natural (Isabelle)
|
