Reseña: Type classes and filters for mathematical analysis in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre análisis matemático titulado Type classes and filters for mathematical analysis in Isabelle/HOL.

Sus autores son Johannes Hölzl, Fabian Immler y Brian Huffman.

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

Su resumen es

The theory of analysis in Isabelle/HOL derives from earlier formalizations that were limited to specific concrete types: ℝ, C and ℝⁿ. Isabelle’s new analysis theory unifies and generalizes these earlier efforts. The improvements are centered on two primary contributions: a generic theory of limits based on filters, and a new hierarchy of type classes that includes various topological, metric, vector, and algebraic spaces. These let us apply many results in multivariate analysis to types which are not Euclidean spaces, such as the extended real numbers, bounded continuous functions, or finite maps.

LMF2013: Resolución en lógica de primer orden

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha presentado la resolución en la lógica de primer orden como ampliación del presentado en el tema 5 para la lógica proposicional.

Las principales diferencias se encuentran en la unificación, separación de variables y factorización.

Las transparencias de esta clase son las del tema 12
Read More “LMF2013: Resolución en lógica de primer orden”

I1M2012: Implementación en Haskell de los grafos mediante matrices. Algoritmos de recorrido de grafos

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado una segunda implementación en Haskell del tipo abstracto de los grafos usando matrices de adyacencia.

Además, hemos estudiado los algoritmos de recorrido de los grafos en profundidad y en anchura.

Las transparencias usadas en la clase son las páginas 19-38 del tema 22:
Read More “I1M2012: Implementación en Haskell de los grafos mediante matrices. Algoritmos de recorrido de grafos”

I1M2012: El TAD de los grafos y su implementación en Haskell mediante vectores de adyacencia

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de los grafos y su implementación en Haskell mediante vectores de adyacencia.

Las transparencias usadas en la clase son las páginas 1-18 del tema 22:
Read More “I1M2012: El TAD de los grafos y su implementación en Haskell mediante vectores de adyacencia”

Reseña: Verifying refutations with extended resolution

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con ACL2 sobre sistemas SAT titulado Verifying refutations with extended resolution.

Sus autores son Marijn J. H. Heule, Warren A. Hunt, Jr. y Nathan Wetzler (de la Universidad de Tejas en Austin).

El trabajo se presentó la semana pasada en el CADE-24 (the 24th International Conference on Automated Deduction).

Su resumen es

Modern SAT solvers use preprocessing and inprocessing techniques that are not solely based on resolution; existing unsatisfiability proof formats do not support SAT solvers using such techniques. We present a new proof format for checking unsatisfiability proofs produced by SAT solvers that use techniques such as extended resolution and blocked clause addition. Our new format was designed with three goals: proofs should be easy to generate, proofs should be compact, and validating proofs must be simple. We show how existing preprocessors and solvers can be modified to generate proofs in our new format. Additionally, we implemented a mechanically-verified proof checker in ACL2 and a proof checker in C for the proposed format.

El correspondiente código ACL2 se encuentra aquí.