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: Formalization of real analysis: A survey of proof assistants and libraries

PorJosé A. Alonso

Se ha publicado un artículo sobre razonamiento formalizado titudado Formalization of real analysis: A survey of proof assistants and libraries.

Sus autores son Sylvie Boldo, Catherine Lelay y Guillaume Melquiond.

Su resumen es

In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability, and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the proof automations these systems provide for real analysis.

Reseña: Formalization of the complex number theory in HOL4

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre números complejos titulado Formalization of the complex number theory in HOL4.

Sus autores son Zhiping Shi, Liming Li, Yong Guan, Xiaoyu Song, Minhua Wu y Jie Zhang.

Su resumen es

In this paper, the theory of complex numbers is formalized and the theorem library of complex numbers is embedded in HOL4, the theorem prover of High Order Logics. The theorem library introduces a data type ℂ by an ℝ × ℝ type abbreviation, and defines arithmetic operations of complex numbers in terms of group and field theories. Moreover, the polar and exponential forms are provided for simplifying the applications in control theory and signal analysis. We define the scalar multiplication of complex numbers and prove some properties about ℝ-module of complex numbers. The theorem library extends the scope of application of HOL4. The developed complex number theory has been released in HOL4 Kananaskis-7.

Reseña: Formal reasoning about finite-state discrete-time Markov chains in HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre procesos de Markov titulado Formal reasoning about finite-state discrete-time Markov chains in HOL.

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

Su resumen es

Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.

La revista en donde que ha publicado el artículo es el Journal of Computer Science and Technology.

Reseña: A string of pearls: Proofs of Fermat’s little theorem

PorJosé A. Alonso

En la CPP12 (The Second International Conference on Certified Programs and Proofs), que comienza el 13 de diciembre, se presentará un trabajo de razonamiento formalizado en HOL4 titulado A string of pearls: Proofs of Fermat’s little theorem.

Sus autores son Hing-Lun Chan (de la Australian National University) y Michael Norrish (del Canberra Research Lab., NICTA).

Su resumen es

We discuss mechanised proofs of Fermat’s Little Theorem in a variety of styles, focusing in particular on an elegant combinatorial “necklace” proof that has not been mechanised previously. What is elegant in prose turns out to be long-winded mechanically, and so we examine the effect of explicitly appealing to group theory. This has pleasant consequences both for the necklace proof, and also for the direct number-theoretic approach.

El código conteniendo las demostraciones en HOL4 se encuentra aquí.