LMF2013: Soluciones lógicas de problemas lógicos

En la clase de hoy del curso Lógica matemática y fundamentos se ha presentado una colección de problemas para mostrar cómo pueden resolverse elementalmente con Prolog.

Los problemas son

  1. Rompecabeza lógico.
  2. La banda de músicos.
  3. Mini sudoku.
  4. Criptoaritmética.
  5. Cuadrados mágicos.
  6. La sucesión de Langford.
  7. Coloraciones de un mapa.
  8. El mono y el plátano.

A continuación se muestran los problemas y sus soluciones
Read More “LMF2013: Soluciones lógicas de problemas lógicos”

I1M2012: Ejercicios de razonamiento sobre programas

En las clases de ayer y hoy Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de la relación 31 en la que se plantean ejercicios de demostración por inducción de propiedades de programas. En concreto,

  • la suma de los n primeros impares es n^2,
  • 1 + 2^0 + 2^1 + 2^2 + … + 2^n = 2^(n+1),
  • todos los elementos de (copia n x) son iguales a x,
  • la equivalencia de las definiciones de factorial con y sin
  • acumulador,
  • amplia xs y = xs ++ [y].
  • numeroDeListasConSuma n = 2^(n-1),
  • fibItAux n (fib k) (fib (k+1)) = fib (k+n),
  • potencia x n == x^n,
  • reverse (xs ++ ys) == reverse ys ++ reverse xs,
  • reverse (reverse xs) = xs,

y por inducción sobre árboles binarios

  • espejo (espejo x) = x,
  • postorden (espejo x) = reverse (preorden x),
  • reverse (preorden (espejo x)) = postorden x,
  • nNodos (espejo x) == nNodos x,
  • length (preorden x) == nNodos x,
  • nNodos x <= 2^(profundidad x) - 1,
  • nHojas x = nNodos x + 1,
  • preordenItAux x ys = preorden x ++ ys

Estos ejercicios corresponden al tema 8 del curso.

Los ejercicios de la relación, junto con sus soluciones, se muestran a continuación
Read More “I1M2012: Ejercicios de razonamiento sobre programas”

Reseña: Automatic data refinement

Se ha publicado un artículo de automatización del razonamiento en Isabelle/HOL titulado Automatic data refinement.

Su autor es Peter Lammich (de la Universidad Técnica de Munich).

El trabajo se presentará en julio en la ITP 2013 (4th Conference on
Interactive Theorem Proving
).

Su resumen es

We present the Autoref tool for Isabelle/HOL, which automatically refines algorithms specified over abstract concepts like maps and sets to algorithms over concrete implementations like red-black-trees, and produces a refinement theorem. It is based on ideas borrowed from relational parametricity due to Reynolds and Wadler.

The tool allows for rapid prototyping of verified, executable algorithms. Moreover, it can be configured to fine-tune the result to the user’s needs. Our tool is able to automatically instantiate generic algorithms, which greatly simplifies the implementation of executable data structures.

Thanks to its integration with the Isabelle Refinement Framework and the Isabelle Collection Framework, Autoref can be used as a backend to a stepwise refinement based development approach, having access to a rich library of verified data structures. We have evaluated the tool by synthesizing efficiently executable refinements for some complex algorithms, as well as by implementing a library of generic algorithms for maps and sets.

La implementación de Autoref, junto con algunos casos de estudio, se encuentra aquí.

I1M2012: Razonamiento sobre programas Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo demostrar propiedades de funciones definidas en Haskell. Los esquemas de demostración estudiados son:

  • por simplificación,
  • por casos,
  • por inducción sobre los números naturales,
  • por inducción sobre listas,
  • por inducción anidada y
  • por generalización e inducción.

Las transparencias usadas en la clase son las del tema 8:
Read More “I1M2012: Razonamiento sobre programas Haskell”