I1M2013: Los problemas de las N reinas y de Hamming en Haskell

PorJosé A. Alonso

En la tercera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos vistos dos aplicaciones de la programación funcional en Haskell: 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 el problema de Hamming (consistente definir una sucesión estrictamente creciente de números tales que el número 1 está en la sucesión y que, si x está en la sucesión, entonces 2*x, 3*x y 5*x también están).

El código del problema de las N reinas es
Read More “I1M2013: Los problemas de las N reinas y de Hamming en Haskell”

I1M2013: Problema del concurso “Cifras y letras” en Haskell

PorJosé A. Alonso

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos desarrollado un programa en Haskell para resolver los problemas aritméticos del concurso Cifras y letras que consisten en dada una sucesión de números naturales y un número objetivo, intentar construir una expresión cuyo valor es el objetivo combinando los números de la sucesión usando suma, resta, multiplicación, división y paréntesis. Además, cada número de la sucesión puede usarse como máximo una vez y todos los números, incluyendo los resultados intermedios tienen que ser enteros positivos (1,2,3,…).

Por ejemplo, dada la sucesión 1, 3, 7, 10, 25, 50 y el objetivo 765, una solución es (1+50)*(25−10). Para el problema anterior existen 780 soluciones. En cambio, con la sucesión anterior y el objetivo 831, no hay solución.

Se empieza formalizando el problema y definiendo una función para reconcer las soluciones. A continuación, se presentan tres soluciones: la primera por fuerza bruta, la segunda mediante generación y evaluación y la tercera con simplificaciones algebraicas. Se termina con una comparación de las tres soluciones.

El código del programa es
Read More “I1M2013: Problema del concurso “Cifras y letras” en Haskell”

A survey of axiom selection as a machine learning problem

PorJosé A. Alonso

Se ha publicado un artículo automatización del razonamiento en Isabelle/HOL titulado A survey of axiom selection as a machine learning problem.

Sus autores son

Su resumen es

Automatic theorem provers struggle to discharge proof obligations of interactive theorem provers. This is partly due to the large number of background facts that are passed to the automatic provers as axioms. Axiom selection algorithms predict the relevance of facts, thereby helping to reduce the search space of automatic provers. This paper presents an introduction to axiom selection as a machine learning problem and describes the challenges that distinguish it from other applications of machine learning.

Properties of random graphs – subgraph containment

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre grafos titulado Properties of random graphs – subgraph containment.

Sus autor es Lars Hupel (de la Univ. Politécnica de Munich).

Su resumen es

Random graphs have been introduced by Erdös and Rényi in [1]. They describe a probability space where, for a fixed number of vertices, each possible edge is present with a certain probability independent from other edges, but with the same probability for each edge. They study what properties emerge when increasing the number of vertices, or as they call it, “the evolution of such a random graph”. The theorem which we will prove here is a slightly different version from that in the first section of that paper.

Here, we are interested in the probability that a random graph contains a certain pattern, for example a cycle or a clique. A very high edge probability gives rise to perhaps too many edges, which is usually undesired since it degrades the performance of many algorithms, whereas a low edge probability might result in a disconnected graph. The central theorem determines a threshold probability such that a higher edge probability will asymptotically almost surely produce a random graph with the desired subgraph.

The proof is outlined in [2, §11.4] and [3, §3]. The work is based on the comprehensive formalization of probability theory in Isabelle/HOL and on a previous definition of graphs in a work by Noschinski [4]. There, Noschinski formalized the proof that graphs with arbitrarily large girth and chromatic number exist. While the proof in this paper uses a different approach, the definition of a probability space on edges turned out to be quite useful.

El trabajo se ha publicado en Archive of Formal Proofs

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.