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