Diferencia entre revisiones de «Razonamiento automático»
De Razonamiento automático (2010-11)
(→Ejemplos) |
(→Razonamiento por inducción sobre listas) |
||
| Línea 15: | Línea 15: | ||
* '''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]]). | ||
| + | * '''Relación 6''': Número de elementos válidos. ([[Rel_6|Enunciado]] y [[Relación 6|Solución]]). | ||
Revisión del 21:43 21 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 Solución).
- Relación 2: Deducción natural en lógica de primer orden. (Enunciado y Solución).