Diferencia entre revisiones de «Razonamiento automático»
De Razonamiento automático (2010-11)
(→Relaciones de ejercicios) |
(→Relaciones de ejercicios) |
||
| Línea 8: | Línea 8: | ||
* [[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]]: Razonamiento por inducción sobre listas. | + | * [[Relación 3]]: Razonamiento por inducción sobre listas: cons inverso y cuantificadores sobre listas. |
| − | * [[Relación 4]]. Sustitución, inversión y eliminación | + | * [[Relación 4]]. Razonamiento por inducción sobre listas: Sustitución, inversión y eliminación. |
Revisión del 12:01 8 feb 2011
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
- Relación 1: Deducción natural en lógica proposicional.
- Relación 2: Deducción natural en lógica de primer orden.
- Relación 3: Razonamiento por inducción sobre listas: cons inverso y cuantificadores sobre listas.
- Relación 4. Razonamiento por inducción sobre listas: Sustitución, inversión y eliminación.