|
Razonamiento Automático (2023-24) |
|
| Temas |
| Ejercicios |
| Sistemas |
| Documentación |
| Trabajos |
| Entrar |
Resolución (Otter)
| Relación 01: | Formalización y resolución en lógica de primer orden |
| Soluciones: Ejercicio 1, Ejercicio 2, Ejercicio 3, Ejercicio 4, Ejercicio 5, Ejercicio 6, Ejercicio 7, Ejercicio 8. | |
| Relación 02: | Razonamiento automático con igualdad |
| Soluciones: Ejercicio 1, Ejercicio 2, Ejercicio 3, Ejercicio 4, Ejercicio 7, Ejercicio 10. |
Inducción (ACL2)
| Relación 03: | Recursión e inducción |
| Relación 04: | Interacción con ACL2 |