|
Razonamiento Automático (2022-23) |
|
| Temas |
| Ejercicios |
| Sistemas |
| Documentación |
| Trabajos |
| Entrar |
Resolución (Otter)
| Relación 01: | Formalización y resolución en lógica de primer orden |
| Ejercicios resueltos en clase: 01-fotografia.in, 02-lanzarote.in, 03-ayuda.in, 04-japones.in, 05-gripe.in, 06-empresa.in, 07-edificio.in, 08-conduccion.in | |
| Relación 02: | Razonamiento automático con igualdad |
| Ejercicios resueltos en clase: 01-fichas.in, 02-fichas.in, 03-fichas.in, 08-fichasAR.in, 09-puertas.in. |
Inducción (ACL2)
| Relación 03: | Recursión e inducción |
| Relación 04: | Interacción con ACL2 |
Deducción natural (Isabelle)
| Relación 05: | Deducción Natural en Isabelle |