Diferencia entre revisiones de «Razonamiento automático»
De Razonamiento automático (2010-11)
(→Razonamiento automático (2010-11)) |
(→Relaciones de ejercicios) |
||
| Línea 8: | Línea 8: | ||
==== Ejercicios de deducción natural ==== | ==== Ejercicios de deducción natural ==== | ||
| − | * '''Relación 1''': Deducción natural en lógica proposicional. ([[Rel_1 | Enunciado]] y [[Relación 1] Solución]). | + | * '''Relación 1''': Deducción natural en lógica proposicional. ([[Rel_1 | Enunciado]] y [[Relación 1] | Solución]). |
| − | * '''Relación 2''': Deducción natural en lógica de primer orden. ([[Rel_2 | Enunciado]] y [[Relación 2] Solución]). | + | * '''Relación 2''': Deducción natural en lógica de primer orden. ([[Rel_2 | Enunciado]] y [[Relación 2] | Solución]). |
==== Razonamiento por inducción sobre listas ==== | ==== Razonamiento por inducción sobre listas ==== | ||
| − | * '''Relación 3''': Cons inverso y cuantificadores sobre listas. ([[Rel_3 | Enunciado]] y [[Relación 3] Solución]). | + | * '''Relación 3''': Cons inverso y cuantificadores sobre listas. ([[Rel_3 | Enunciado]] y [[Relación 3] | Solución]). |
| − | * '''Relación 4''': Sustitución, inversión y eliminación. ([[Rel_4 | Enunciado]] y [[Relación 4] Solución]). | + | * '''Relación 4''': Sustitución, inversión y eliminación. ([[Rel_4 | Enunciado]] y [[Relación 4] | Solución]). |
| − | * '''Relación 5''': Menor posición válida. ([[Rel_5 | Enunciado]] y [[Relación 5] Solución]). | + | * '''Relación 5''': Menor posición válida. ([[Rel_5 | Enunciado]] y [[Relación 5] | Solución]). |
Revisión del 00:41 15 feb 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 [[Relación 1] | Solución]).
- Relación 2: Deducción natural en lógica de primer orden. ( Enunciado y [[Relación 2] | Solución]).