RA2013: Verificación de la ordenación por inserción con Isabell/HOL
En la segunda parte de la clase de hoy del curso de Razonamiento automático se estudiado cómo verificar formalmente con Isabelle/HOL la corrección de la ordenación por inserción
La correspondiente teoría se muestra a continuación
Read More “RA2013: Verificación de la ordenación por inserción con Isabell/HOL”