DAO (Demostración asistida por ordenador) DAO (Demostración asistida por ordenador)

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).
• Relación 2: Argumentación proposicional con Isabelle/HOL. (Enunciado).
• Relación 3: Eliminación de conectivas. (Enunciado).
• Relación 4: Deducción natural en lógica de primer con Isabelle/HOL. (Enunciado).
• Relación 5: Argumentación en lógica de primer con Isabelle/HOL. (Enunciado).
• Relación 6: Argumentación en lógica de primer orden e igualdad con Isabelle/HOL. (Enunciado).
• Relación 7: Programación funcional en Isabelle/HOL. (Enunciado).
• Relación 8: Razonamiento sobre programas en Isabelle/HOL. (Enunciado).
• Relación 9: Cons inverso. (Enunciado).
• Relación 10: Cuantificadores sobre listas. (Enunciado).
• Relación 11: Sustitución, inversión y eliminación. (Enunciado).
• Relación 12: Menor posición válida. (Enunciado).
• Relación 13: Número de elementos válidos. (Enunciado).
• Relación 14: Contador de occurrencias. (Enunciado).
• Relación 15: Suma y aplanamiento de listas. (Enunciado).
• Relación 16: Conjuntos mediante listas. (Enunciado).
• Relación 17: Ordenación de listas por inserción. (Enunciado).
• Relación 18: Ordenación de listas por mezcla. (Enunciado).
• Relación 19: Recorridos de árboles. (Enunciado).
• Relación 20: Plegados de listas y de árboles. (Enunciado).
• Relación 21: Árboles binarios completos. (Enunciado).
• Relación 22: Diagramas de decisión binarios. (Enunciado).
• Relación 23: Representación de fórmulas proposicionales mediante polinomios. (Enunciado).