Reseña: ForMaRE – formal mathematical reasoning in economics

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado a la economía titulado ForMaRE – formal mathematical reasoning in economics.

Sus autores son Manfred Kerber, Christoph Lange y Colin Rowat (de la Universidad de Birmingham) y lo presentarán hoy en el ARW2013 (20th Automated Reasoning Workshop).

Su resumen es

We present the ForMaRE project which applies FORmal MAthematical REasoning to economics. Theoretical economics makes use of mathematical proof and we seek to increase confidence in these theoretical results by applying formal mathematical reasoning. This will lead on the one hand to new challenge problems in formal reasoning. On the other hand we are conducting research that connects economics and formal methods. We will discuss some areas of interest such as game theory and auctions, where we are currently building a toolbox of formalizations.

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: Homotopy limits in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Homotopy limits in Coq.

Sus autores son Jeremy Avigad (de la Carnegie Mellon University), Krzysztof Kapulkin (de la Univ. de Pittsburgh) y Peter LeFanu Lumsdaine.

Su resumen es

Working in Homotopy Type Theory, we provide a systematic study of basic homotopy limits and related constructions. The entire development has been formally verified in the Coq interactive proof assistant.

Las teorías en Coq correspondientes al artículo se encuentra aquí.

Reseña: Formalizing the confluence of orthogonal rewriting systems

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en PVS sobre reescritura titulado Formalizing the confluence of orthogonal rewriting systems.

Sus autores son Ana Cristina Rocha Oliveira y Mauricio Ayala-Rincón (de la Universidad de Brasilia)

Su resumen es

Orthogonality is a discipline of programming that in a syntactic manner guarantees determinism of functional specifications. Essentially, orthogonality avoids, on the one side, the inherent ambiguity of non determinism, prohibiting the existence of different rules that specify the same function and that may apply simultaneously (non-ambiguity), and, on the other side, it eliminates the possibility of occurrence of repetitions of variables in the left-hand side of these rules (left linearity). In the theory of term rewriting systems (TRSs) determinism is captured by the well-known property of confluence, that basically states that whenever different computations or simplifications from a term are possible, the computed answers should coincide. Although the proofs are technically elaborated, confluence is well-known to be a consequence of orthogonality. Thus, orthogonality is an important mathematical discipline intrinsic to the specification of recursive functions that is naturally applied in functional programming and specification. Starting from a formalization of the theory of TRSs in the proof assistant PVS, this work describes how confluence of orthogonal TRSs has been formalized, based on axiomatizations of properties of rules, positions and substitutions involved in parallel steps of reduction, in this proof assistant. Proofs for some similar but restricted properties such as the property of confluence of non-ambiguous and (left and right) linear TRSs have been fully formalized.

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.