Reseña: A certified proof of the Cartan Fixed Point Theorems

PorJosé A. Alonso

Gianni Ciolli, Graziano Gentili y Marco Maggesi han publicado el artículo A Certified Proof of the Cartan Fixed Point Theorems en el Journal of Automated Reasoning. Una versión del artículo puede leerse aquí.

Los autores son profesores del Departamento de Matemáticas “Ulisses Dini” de la Universidad de Florencia. Los dos primeros son especialistas en geometría algebraica y análisis complejo y el tercero trabaja en razonamiento automático con Coq y HOL Light.

El objetivo del artículo es la aplicación del razonamiento formalizado a temas de investigación de la matemática contemporánea. Para ello han elegido como objetivo la formalización de los teoremas de Cartan del punto fijo, demostrados por Henri Cartan en 1930. Los teoremas elegidos son relativamente recientes y de gran importancia en el análisis complejos y campos relacionados.
Read More “Reseña: A certified proof of the Cartan Fixed Point Theorems”

Executable Multivariate Polynomials

PorJosé A. Alonso

Christian Sternagel y René Thiemann han publicado en The Archive of Formal Proofs el artículo Executable Multivariate Polynomials.

El artículo es parte del proyecto IsaFoR/CeTA (Isabelle Formalization of Rewriting / Certified Termination Analysis) cuyo objetivo es la formalización en Isabelle de técnicas de terminación. Los ficheros del proyecto se encuentran aquí.

Una de las técnicas usadas para demostrar la terminación de sistemas de reescritura se basa en las interpretaciones polinómicas.

En el artículo Executable Multivariate Polynomials se presenta una formalización en Isabelle de los polinomios con varias variables con coeficientes en un semianillo ordenado. Se definen las operaciones de polinomios (suma, multiplicación y sustitución) y la ordenación de polinomios. La formalización también incluye el criterio de Neurauter, Zankl y Middeldorp monotocidad de interpretaciones polinómicas sobre los naturales.

Formal Power Series

PorJosé A. Alonso

Acaba de publicarse un nuevo artículo de razonamiento formalizado. El artículo es Formal Power Series publicado por Amine Chaieb en el Journal of Automated Reasoning.

El resumen que hace el autor del artículo es el siguiente: We present a formalization of the topological ring of formal power series in Isabelle/HOL. We also formalize formal derivatives, division, radicals, composition and reverses. As an application, we show how formal elementary and hyper-geometric series yield elegant proofs for some combinatorial identities. We easily derive a basic theory of polynomials. Then, using a generic formalization of the fraction field of an integral domain, we obtain formal Laurent series and rational functions for free.

La formalización completa se encuentra en Theory Formal Power Series

Razonamiento formalizado en análisis numérico

PorJosé A. Alonso

Hoy se ha publicado en arXiv el artículo Formal Proof of a Wave Equation Resolution Scheme: the Method Error escrito por Sylvie Boldo (INRIA Saclay – Ile de France, LRI), Francois Clement (INRIA Rocquencourt), Jean-Christophe Filliâtre (INRIA Saclay – Ile de France, LRI), Micaela Mayero (LIPN, INRIA Rhône-Alpes / LIP Laboratoire de l’Informatique du Parallélisme), Guillaume Melquiond (INRIA Saclay – Ile de France, LRI) y Pierre Weis (INRIA Rocquencourt).

En este trabajo se presenta una formalización en Coq de una parte del conocimiento matemático más usado en las ingeniería: las ecuaciones diferenciales. Curiosamente las ecuaciones diferenciales apenas se han tratado dentro del razonamiento formalizado.

Read More “Razonamiento formalizado en análisis numérico”

Reseña – A Formalization of the Knuth–Bendix(–Huet) Critical Pair Theorem

PorJosé A. Alonso

El día 21 se publicó en el Journal of Automated Reasoning el artículo A Formalization of the Knuth–Bendix(–Huet) Critical Pair Theorem/a> escrito por André L. Galdino y Mauricio Ayala Rincón. En el trabajo se presenta una formalización en PVS del teorema de pares críticos. También es pública la teoría PVS con la formalización.

Este trabajo es la continuación de anteriores trabajos de los autores

  1. A Theory for Abstract Reduction Systems in PVS
  2. Verification of Newman’s and Yokouchi Lemmas in PVS
  3. A PVS theory for Term Rewriting Systems

Todos estos trabajos son extensiones de la tesis de André L. Galdino Uma formalização da teoria de reescrita em linguagem de ordem superior dirigida por Mauricio Ayala Rincón. En la tesis se realiza una formalización en PVS de los sistemas de reescritura semejante a la realizada en ACL2 por José Luis Ruiz Reina en su tesis Una teoría computacional acerca de la lógica ecuacional (formalización ACL2 de la lógica ecuacional y demostración automática de sus propiedades).