I1M2019: Introducción a la programación imperativa con Python

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha presentado una introducción a la programación con Python.

En la presentación se ha seguido el siguiente guión:

  1. Python como calculadora
  2. Variables y asignaciones
  3. Bloques de instrucciones
  4. Definición de funciones
  5. Escritura y lectura
  6. La estructura condicional: condicionales simples y múltiple.
  7. Estructuras iterativas: bucles mientras, hasta y para.
  8. Recursión

En la presentación se han usado ejemplos anteriormente estudiados con Haskell. Se ha remarcado la analogías y diferencias entre Haskell y Python.

Finalmente, se ha definido la función de Takeuchi en Python y en Haskell
y se ha comparado la eficiencia.

El cuaderno de la presentación se encuentra Binder.

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”