Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

Trabajos propuestos

En esta sección se publicarán los trabajos propuestos en la asignatura.

• T1_1: Verificación del algoritmo de ordenación por inserción en Isabelle/HOL. (Enunciado).
• T1_2: Verificación del algoritmo de ordenación por mezcla en Isabelle/HOL. (Enunciado).
• T1_3: Verificación del algoritmo de ordenación rápida en Isabelle/HOL. (Enunciado).