Verified AIG algorithms in ACL2

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en ACL2 titulado Verified AIG algorithms in ACL2.

Sus autores son

Su resumen es

And-Inverter Graphs (AIGs) are a popular way to represent Boolean functions (like circuits). AIG simplification algorithms can dramatically reduce an AIG, and play an important role in modern hardware verification tools like equivalence checkers. In practice, these tricky algorithms are implemented with optimized C or C++ routines with no guarantee of correctness. Meanwhile, many interactive theorem provers can now employ SAT or SMT solvers to automatically solve finite goals, but no theorem prover makes use of these advanced, AIG-based approaches.

We have developed two ways to represent AIGs within the ACL2 theorem prover. One representation, Hons-AIGs, is especially convenient to use and reason about. The other, Aignet, is the opposite; it is styled after modern AIG packages and allows for efficient algorithms. We have implemented functions for converting between these representations, random vector simulation, conversion to CNF, etc., and developed reasoning strategies for verifying these algorithms.

Aside from these contributions towards verifying AIG algorithms, this work has an immediate, practical benefit for ACL2 users who are using GL to bit-blast finite ACL2 theorems: they can now optionally trust an off-the-shelf SAT solver to carry out the proof, instead of using the built-in BDD package. Looking to the future, it is a first step toward implementing verified AIG simplification algorithms that might further improve GL performance

El trabajo se ha presentado en el ACL2 2013 (Eleventh International Workshop on the ACL2 Theorem Prover and Its Applications).

Polygonal numbers in Mizar

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Mizar titulado Polygonal numbers in Mizar.

Su autor es Adam Grabowski (de la Universidad de Białystok, Polonia).

Su resumen es

In the article the formal characterization of triangular numbers (famous from [14] and words “EYPHKA! num = ∆ + ∆ + ∆”) [16] is given. Our primary aim was to formalize one of the items (42) from Wiedijk’s Top 100 Mathematical Theorems list, namely that the sequence of sums of reciprocals of triangular numbers converges to 2 and this Mizar representation was written in 2007. As the Mizar language evolved and attributes with arguments were implemented, we decided to extend these lines and we characterized polygonal numbers.

We formalized centered polygonal numbers, the connection between triangular and square numbers, and also some equalities involving Mersenne primes and perfect numbers. We gave also explicit formula to obtain from the polygonal number its ordinal index. Also selected congruences modulo 10 were enumerated. Our work basically covers the Wikipedia item for triangular numbers and
the Online Encyclopedia of Integer Sequences (http://oeis.org/A000217).

An interesting related result [15] could be the proof of Lagrange’s four-square theorem or Fermat’s polygonal number theorem [30].

El artículo se publicará en la revista Formalized Mathematics.

Introducción a la demostración asistida por ordenador con Isabelle/HOL

PorJosé A. Alonso

En el libro Introducción a la demostración asistida por ordenador con Isabelle/HOL he recopilado los temas y relaciones de ejercicios del curso de Razonamiento automático (2012-13).

El curso es una introducción a la demostración asistida por ordenador con Isabelle/HOL y consta de tres niveles.

En el primer nivel se presenta la formalización de las demostraciones por deducción natural. La presentación se basa en la realizada en los cursos de Lógica informática (de 2º del Grado en Informática) y Lógica matemática y fundamentos (de 3º del Grado en Matemáticas), en concreto en los temas de deducción natural proposicional y de primer orden. En este nivel se incluye los 3 primeros temas y las 6 primeras relaciones de ejercicios.

En el segundo nivel se presenta la programación funcional en Isabelle/HOL y el razonamiento sobre programas. La presentación se basa en la introducción a la programación con Haskell realizada en los cursos de Informática (de 1º del Grado en Matemáticas) y Programación declarativa (de 3º del Grado en Informática), en concreto en el tema 8 (para el razonamiento sobre programas) y en los restantes 9 primeros temas (para la programación funcional). En este nivel se incluye los temas 4, 5 y 6 y las relaciones de ejercicios desde la 7 a la 21.

En el tercer nivel se presentan casos de estudios y extensiones de la lógica para trabajar con conjuntos, relaciones y funciones. En este nivel se incluyen los temas 7 y 8 y las relaciones de ejercicios 22 y 23.

Tanto los temas como las relaciones de ejercicios se presentan como teorías de Isabelle/HOL (versión Isabelle2013). Conforme se necesitan se va comentando los elementos del Isabelle/HOL.

De Isabelle2013 se dispone se dispone de versiones libres para Linux, Windows y Mac OS X. Para instalarlo basta seguir la guía de instalación.

Los números de Ulam en Haskell

PorJosé A. Alonso

Los números de Ulam son los elementos de la sucesión u(n) definida por u(1) = 1, u(2) = 2 y, para n > 2, u(n) es el entero más pequeño que se puede escribir exactamente de una forma como suma de dos términos anteriores diferentes entre sí.

Según la definición, 3=1+2 es un número de Ulam y 4=1+3 también es un número de Ulam (la suma 4=2+2 no cuenta porque los términos previos deben ser distintos). El entero 5 no es un número de Ulam porque 5=1+4=2+3.

Los primeros términos de la sucUlam son: 1, 2, 3, 4, 6, 8, 11, 13, 16, 18, 26, 28, 36, 38, 47, 48, 53, 57, 62, 69, 72, 77, 82, 87, 97, 99.

Esta sucesión fue definida por el matemático polaco Stanislaw Ulam y
publicada en SIAM Review en 1964.

A partir de los artículos de la Wikipedia y de MathWorld sobre los números de Ulam elaborado la siguiente relación de ejercicios de Haskell para la asignatura de Informática de 1º del Grado en Matemáticas.

En la relación se presentan cuatro definiciones de los números de Ulam, se compara su eficiencia, se muestra algunas de sus propiedades terminando con los números de Ulam generalizados.
Read More “Los números de Ulam en Haskell”

Generic datatypes à la carte

PorJosé A. Alonso

Se ha publicado un artículo de automatización del razonamiento en Coq titulado Generic datatypes à la carte.

Sus autores son Steven Keuchel y Tom Schrijvers (de la Universidad de Gante, Bélgica).

Su resumen es

Formal reasoning in proof assistants, also known as mechanization, has high development costs. Building modular reusable components is a key issue in reducing these costs. A stumbling block for reuse is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory à la Carte (MTC) framework in the context of programming language meta-theory. However, MTC’s use of extensible Church-encodings is unsatisfactory.

This paper takes a better approach to the problem with datatype- generic programming (DGP). It applies well-known DGP techniques to represent modular datatypes, to build functions from functor algebras with folds and to compose proofs from proof algebras by means of induction. Moreover, for certain functionality and proofs our approach can achieve more reuse than MTC: instead of composing modular components we provide a single generic definition once and for all.

El correspondiente código en Coq se encuentra aquí.

El trabajo se presentará en el WGP 2013 (9th ACM SIGPLAN Workshop on Generic Programming).