RA2019: Ejercicios de razonamiento estructurado sobre programas en Isabelle/HOL

En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 3ª relación de ejercicios de razonamiento estructurado sobre programas. Para cada propiedad se dan tres demostraciones en Isabelle/HOL: la primera automática, la segunda estructurada y la tercera totalmente detallada mostrando todos los lemas de HOL que se utilizan en cada paso.

La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2019: Ejercicios de razonamiento estructurado sobre programas en Isabelle/HOL”

RA2019: Razonamiento por casos y por inducción en Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático hemos profundizado en el estudio de las demostraciones por casos y por inducción. En concreto, se ha estudiado

  • el razonamiento por casos booleanos,
  • el razonamiento por casos booleanos sobre una variable,
  • el razonamiento por casos sobre listas,
  • el razonamiento por inducción sobre números naturales con patrones,
  • el razonamiento sobre definiciones con existenciales,
  • el uso de librerías auxiliares (como Parity) y
  • el uso de otros métodos de demostración (como presburg).

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2019: Razonamiento por casos y por inducción en Isabelle/HOL”

I1M2019: De la matemática a la máquina

En la segunda parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se ha comentado cómo los se pueden representar los conceptos matemáticos en los ordenadores.

Para ello se ha visto cómo la definición de factorial se puede definir en distintos paradigmas desde la matemática al código máquina. Las definiciones consideradas han sido

  • En matemáticas

  • En programación funcional (Haskell).

  • En programación imperativa (C).

  • En ensamblador.

  • En código máquina.

La exposición se ha basado en el artículo From math to machine: translating a function to machine code de Brian Steffens.