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.

Reseña: On the formalization of continuous-time Markov chains in HOL

PorJosé A. Alonso

Se ha publicado un trabajo de razonamiento formalizado en HOL4 titulado On the formalization of continuous-time Markov chains in HOL.

Sus autores son Liya Liu, Osman Hasan y Sofiène Tahar (de la Concordia University, Montreal, Canadá).

Su resumen es

Continuous-time Markov chain has been extensively applied to model diverse real-world systems. The analysis of these systems has been conducted using conventional simulation technique and computer algebra systems, more recently, probabilistic model checking. However, these methods either cannot guarantee accurate analysis or are not scalable due to the unacceptable computation consumption. As a complemental technique, theorem proving is proposed to reason about continuous-time Markov chain using HOL theorem proving. To our best knowledge, the formalization of continuous-time Markov chain has not been found in any theorem prover. In this report, we provide the idea on the formal definition of continuous-time Markov chain and two of its formally verified properties as the first step to formalize the continuous-time Markov chain theory. Also, we present the next step and the predict the potential challenges in the formalization process. Finally, a certain of applications are listed to be targeted using the formalized continuous-time Markov chain.

Reseña: Graph theory

PorJosé A. Alonso

Se ha publicado un nuevo artículo de razonamiento formalizado en Isabelle/HOL titulado Graph theory.

Su autor es Lars Noschinski (de la Univrsidad Técnica de Munich).

Su resumen es

This development provides a formalization of directed graphs, supporting (labelled) multi-edges and infinite graphs. A polymorphic edge type allows edges to be treated as pairs of vertices, if multi-edges are not required. Formalized properties are i.a. walks (and related concepts), connectedness and subgraphs and basic properties of isomorphisms.

This formalization is used to prove characterizations of Euler Trails, Shortest Paths and Kuratowski subgraphs.

Definitions and nomenclature are based on Digraphs: Theory, algorithms and applications (by J. Bang-Jensen and G. Gutin).

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

Reseña: Formalization of incremental simplex algorithm by stepwise refinement

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Formalization of incremental simplex algorithm by stepwise refinement.

Sus autores son Mirko Spasić and Filip Marić (de la Universidad de Belgrado).

Su resumen es

We present an Isabelle/HOL formalization and total correctness proof for the incremental version of the Simplex algorithm which is used in most state-of-the-art SMT solvers. Formalization relies on stepwise program and data refinement, starting from a simple specification, going through a number of fine refinement steps, and ending up in a fully executable functional implementation. Symmetries present in the algorithm are handled with special care.

El trabajo se presentó en el FM2012 (18th International Symposium on Formal Methods) y las transparencias de la presentación se encuentran aquí.

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

Reseña: Coinductive pearl: Modular first-order logic completeness

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado Coinductive pearl: Modular first-order logic completeness.

Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Universidad Técnica de Munich).

Su resumen es

Codatatypes are unfortunately still missing in many programming languages and proof assistants. We make a case for their usefulness by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. Codatatypes help capture the essence of the proof, which establishes an abstract property of derivation trees independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation, especially for readers acquainted with lazy data structures. The proof is formalized in Isabelle/HOL and demonstrates the recently introduced definitional package for codatatypes and its integration with Isabelle’s Haskell code generator.

El código de las teorías Isabelle correspodientes se encuentra aquí.