Ejercicios RA2013
De DAO (Demostración asistida por ordenador)
Revisión del 16:53 22 oct 2013 de Jalonso (discusión | contribuciones) (Deshecha la edición 147 de Jalonso (disc.))
Ejercicios de Demostración asistida por ordenador
En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deben tomarse como definitivas.
- Relación 1: Deducción natural en lógica proposicional con Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 2: Argumentación proposicional con Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 3: Eliminación de conectivas. (Enunciado y Solución colaborativa).
- Relación 4: Deducción natural en lógica de primer con Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 5: Argumentación en lógica de primer con Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 6: Argumentación en lógica de primer orden e igualdad con Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 7: Programación funcional en Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 8: Razonamiento sobre programas en Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 9: Cons inverso. (Enunciado y Solución colaborativa).
- Relación 10: Cuantificadores sobre listas. (Enunciado y Solución colaborativa).
- Relación 11: Sustitución, inversión y eliminación. (Enunciado y Solución colaborativa).
- Relación 12: Menor posición válida. (Enunciado y Solución colaborativa).
- Relación 13: Número de elementos válidos. (Enunciado y Solución colaborativa).
- Relación 14: Contador de occurrencias. (Enunciado y Solución colaborativa).
- Relación 15: Suma y aplanamiento de listas. (Enunciado y Solución colaborativa).
- Relación 16: Conjuntos mediante listas. (Enunciado y Solución colaborativa).
- Relación 17: Ordenación de listas por inserción. (Enunciado y Solución colaborativa).
- Relación 18: Ordenación de listas por mezcla. (Enunciado y Solución colaborativa).
- Relación 19: Recorridos de árboles. (Enunciado y Solución colaborativa).
- Relación 20: Plegados de listas y de árboles. (Enunciado y Solución colaborativa).
- Relación 21: Árboles binarios completos. (Enunciado y Solución colaborativa).
- Relación 22: Diagramas de decisión binarios. (Enunciado y Solución colaborativa).
- Relación 23: Representación de fórmulas proposicionales mediante polinomios. (Enunciado y Solución colaborativa).