Ver el código de «Ejercicios de "Razonamiento automático (2011-12)"» - Razonamiento automático (2010-11)

 __NOTOC__
== Ejercicios de "Razonamiento automático" ==

=== 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. ([[Rel_1|Enunciado]]).
* '''Relación 2''': Deducción natural en lógica de primer orden. ([[Rel_2|Enunciado]]).

==== Razonamiento por inducción sobre listas ====
* '''Relación 3''': Cons inverso y cuantificadores sobre listas. ([[Rel_3|Enunciado]]).
* '''Relación 4''': Sustitución, inversión y eliminación. ([[Rel_4|Enunciado]]).
* '''Relación 5''': Menor posición válida. ([[Rel_5|Enunciado]]).
* '''Relación 6''': Número de elementos válidos. ([[Rel_6|Enunciado]]).
* '''Relación 7''': Contador de occurrencias. ([[Rel_7|Enunciado]]).
* '''Relación 8''': Suma y aplanamiento de listas. ([[Rel_8|Enunciado]]).

==== Ejercicios complementarios ====
* '''Relación 9''': Deducción natural en lógica proposicional. ([[Rel_9|Enunciado]]).
* '''Relación 10''': Deducción natural en lógica de primer orden. ([[Rel_10|Enunciado]]).
* '''Relación 11''': Razonamiento sobre programas. ([[Rel_11|Enunciado]]).