Anuncio: Reducing the size of resolution proofs in linear time

PorJosé A. Alonso

Se ha publicado el artículo Reducing the size of resolution proofs in linear time en la revista International Journal on Software Tools for Technology Transfer (STTT).

Una versión del artículo puede leerse aquí

Los autores del artículo son Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory, Ohad Shacham y Ofer Strichman. Los tres primeros trabajaban en IBM R&D Labs in Israel y el cuarto en Technion – Israel Institute of Technology.

El resumen del artículo es
Read More “Anuncio: Reducing the size of resolution proofs in linear time”

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.

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).