Diferencia entre revisiones de «Razonamiento automático»
De Razonamiento automático (2010-11)
(→Razonamiento automático (2010-11)) |
(→Relaciones de ejercicios) |
||
| Línea 18: | Línea 18: | ||
* '''Relación 7''': Contador de occurrencias. ([[Rel_7|Enunciado]] y [[Relación 7|Solución]]). | * '''Relación 7''': Contador de occurrencias. ([[Rel_7|Enunciado]] y [[Relación 7|Solución]]). | ||
* '''Relación 8''': Suma y aplanamiento de listas. ([[Rel_8|Enunciado]] y [[Relación 8|Solución]]). | * '''Relación 8''': Suma y aplanamiento de listas. ([[Rel_8|Enunciado]] y [[Relación 8|Solución]]). | ||
| + | |||
| + | ==== Ejercicios complementarios ==== | ||
| + | * '''Relación 9''': Deducción natural en lógica proposicional. ([[Rel_9|Enunciado]] y [[Relación 9|Solución]]). | ||
Revisión del 22:53 14 mar 2011
Sumario
Razonamiento automático (2010-11)
Ejemplos
- Deducción natural en lógica proposicional con Isabelle/Isar.
- Deducción natural en lógica de primer orden con Isabelle/Isar.
Relaciones de ejercicios
Ejercicios de deducción natural
- Relación 1: Deducción natural en lógica proposicional. (Enunciado y Solución).
- Relación 2: Deducción natural en lógica de primer orden. (Enunciado y Solución).
Razonamiento por inducción sobre listas
- Relación 3: Cons inverso y cuantificadores sobre listas. (Enunciado y Solución).
- Relación 4: Sustitución, inversión y eliminación. (Enunciado y Solución).
- Relación 5: Menor posición válida. (Enunciado y Solución).
- Relación 6: Número de elementos válidos. (Enunciado y Solución).
- Relación 7: Contador de occurrencias. (Enunciado y Solución).
- Relación 8: Suma y aplanamiento de listas. (Enunciado y Solución).