Razonamiento automático (2010-11) Razonamiento automático (2010-11)

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]).

Razonamiento por inducción sobre listas

• Relación 3: Cons inverso y cuantificadores sobre listas. ( Enunciado y [[Relación 3] | Solución]).
• Relación 4: Sustitución, inversión y eliminación. ( Enunciado y [[Relación 4] | Solución]).
• Relación 5: Menor posición válida. ( Enunciado y [[Relación 5] | Solución]).