LMF2013: Estrategias de resolución proposicional

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos hemos continuado la búsqueda de la automatización del razonamiento.

Después de haber visto en la clase anterior el algoritmo de resolución por saturación, hemos estudiado distintas estrategias cuyo objetivo es mejorar la búsqueda de la refutación por resolución.

Las estrategias estudiadas son la resolución positiva, la resolución negativa, la resolución unitaria, la resolución por entradas y la resolución lineal.

Además, se ha presentado la estrategia por pesos y propagación unitaria.

Finalmente, como sistema de demostración por resolución se ha presentado el Prover9.

Las transparencias de esta clase son las páginas 25 a 37 del tema 5
Read More “LMF2013: Estrategias de resolución proposicional”

I1M2012: El problema de las N reinas en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el problema de las reinas (consistente en colocar N reinas en un tablero de dimensiones N por N de forma que no se encuentren más de una en la misma línea: horizontal, vertical o diagonal) y su programación en Haskell.

El código del problema de las N reinas es
Read More “I1M2012: El problema de las N reinas en Haskell”

I1M2012: Ejercicios sobre matrices en Haskell (2)

PorJosé A. Alonso

En la clase hoy Informática de 1º del Grado en Matemáticas hemos continuando comentado las soluciones de los ejercicios sobre vectores y matrices en Haskell de la relación 26. Concretamente, de los ejercicios para

  • calcular la traspuesta de una matriz (ej. 14),
  • decidir si una matriz es cuadrada (ej. 15),
  • decidir si una matriz es simétrica (ej. 16),
  • calcular la diagonal principal de una matriz (ej. 17),
  • calcular la diagonal secundaria de una matriz (ej. 18) y
  • calcular la submatriz obtenida suprimiendo una fila y una columna (ej. 19).

Los ejercicios de la relación, junto con las soluciones de los 19 primeros, se muestran a continuación
Read More “I1M2012: Ejercicios sobre matrices en Haskell (2)”

Reseña: Formalizing Turing machines

PorJosé A. Alonso

Se ha publicado un trabajo de razonamiento formalizado con Matita sobre máquinas de Turing titulado Formalizing Turing machines.

Sus autores son Andrea Asperti y Wilmer Ricciotti (de la Universidad de Bolonia, Italia).

Su resumen es

We discuss the formalization, in the Matita Theorem Prover, of a few, basic results on Turing Machines, up to the existence of a (certified) Universal Machine. The work is meant to be a preliminary step towards the creation of a formal repository in Complexity Theory, and is a small piece in our Reverse Complexity program, aiming to a comfortable, machine independent axiomatization of the field.

El trabajo se presentó en el WoLLIC 2012 (19th Workshop on Logic, Language, Information and Computation). La transparencias de la presentación se encuentran aquí.

Reseña: Light-weight containers for Isabelle: efficient, extensible, nestable

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en Isabelle/HOL titulado Light-weight containers for Isabelle: efficient, extensible, nestable.

Su autor es Andreas Lochbihler (del ETH Zürich).

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

Su resumen es

In Isabelle/HOL, we develop an approach to efficiently implement container types such as sets and maps in generated code. Thanks to type classes and refinement during code generation, our light-weight framework is flexible, extensible, and easy to use. To support arbitrary nesting of containers, we devise an efficient linear order on sets that can even compare complements and non-complements. Our evaluation shows that it is both efficient and usable.

Los códigos de las correspondientes teorías en Isabelle/HOL se encuentran aquí.