Representación del conocimiento político

PorJosé A. Alonso

Uno de los campos de estudio de la lógica computacional es la representación del conocimiento que suele abordar mi compañero Joaquín Borrego en su blog Ontoblogia.

Uno de los problemas que se presentan en la representación del conocimiento, como señala J.A. Chaves en Reflexiones acerca de las teorías sobre ética en la representación del conocimiento, es la adaptación de las expresiones que evolucionan a lo largo de tiempo por la presión de lo “políticamente correcto”.

En estos días estamos asistiendo a una de dichas evoluciones: se está transformando la expresión “cementerio nuclear” en “almacén temporal centralizado”.
Read More “Representación del conocimiento político”

Demostración de propiedades de los indefinibles

PorJosé A. Alonso

Gustavo Piñeiro es un matemático argentino autor, junto con Guillermo Martínez, del libro Gödel para todos. Además, escribe el blog El topo lógico. En el último artículo en su blog (Paradojas del infinito (I)) trata de los números definibles e indefinibles, entendiendo que un número es definible si existe una propiedad expresada mediante una frase en castellano tal que sólo la verifica dicho número.

La existencia de los números definibles se demuestra mostrando algunos de dichos números (por ejemplo, el número 0 es el cardinal del conjunto de los elementos x tales que x es distinto de x). La existencia de los números indefinibles se sigue de que el conjunto de los números definibles es numerable y el conjunto de los números reales es infinito no numerable.

A pesar de haber un conjunto no numerable de números indefinibles, no podemos definir ninguno de ellos. Sin embargo, se puede demostrar que tienen algunas propiedades. Por ejemplo, la suma de un número definible y otro indefinible es un número indefinible.

Sería interesante ver la formalización de estas propiedades en los sistemas de razonamiento usados en nuestro grupo.

Certificación computacional del conocimiento matemático

PorJosé A. Alonso

Esta entrada está dedicada a los antecentes de la certificación computacional del conocimiento matemático en estilo declarativo.

Por lo que respecta a la verificación declarativa, sus raices se encuentran en el trabajo realizado en el proyecto Mizar. El proyecto Mizar comenzó en el 1973 como un intento de reconstruir la matemática en un entorno computacionalmente certificable. Los teoremas demostrados dentro del proyecto Mizar se encuentran fundamentalmente en la Mizar Mathematical Library y en la revista Formalized Mathematics que se publica desde el año 1990. El sistema Mizar no es automático sino que es sólo un verificador. Por contra, los sistemas de demostración no disponían de modos de demostración declararativa hasta que M. Wenzel creó Isar (Intelligible semi-automated reasoning). Isar está construido sobre el sistema Isabelle. Isabelle es un asistente de prueba genérico desarrollado por L. Paulson (en la Universidad de Cambridge) y T. Nipkow (en la Universidad Politécnica de Munich). Las teorías formalizadas en Isabelle/Isar se encuentran fundamentalmente en la biblioteca de Isabelle2009-1, en la revista The Archive of Formal Proofs y en la IsarMathLib (A library of formalized mathematics for Isabelle/ZF theorem proving environment).

Por lo que respecta a la certificación computacional del conocimiento
matemático los antecedentes pueden situarse en el 1993 con la publicación del manifiesto del proyecto QED impulsado por Bob Boyer y la revisión del proyecto QED en 2007 por F. Wiedijk. Actualmente se han demostrado muchos teoremas matemáticos importantes, como puede comprobarse en Formalizing 100 Theorems, en la NASA Langley PVS Libraries y en The Coq Users’ Contributions. Entre los teoremas formalmente certificados podemos citar el teorema de de la distribución de los números primos, el teorema de los cuatro colores y el teorema de la curva de Jordan. Nuestro grupo posee experiencia en la certificación de teoremas matemáticos habiendo certificado en ACL2 y PVS, entre otros, el lema de Newman, el teorema de Knuth-Bendix, el teorema de corrección del algoritmo de Buchberger, el teorema de Bezem de completitud de la resolución proposicional y el teorema de completitud de la resolución SLD.

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”

SBMF 2010: 13th Brazilian Symposium on Formal Methods

PorJosé A. Alonso

El SBMF 2010: 13th Brazilian Symposium on Formal Methods se celebrará en Natal (Rio Grande do Norte, Brazil) del 8 al 12 de Noviembre.

Entre los temas del congreso relacionados con el trabajo de nuestro grupo están:

  1. Especificación y modelización.
  2. Técnicas de abstracción, modularización y refinamiento.
  3. Demostración automática de teoremas.
  4. Certificación de software.
  5. Enseñanza de, y con, métodos formales.
  6. Desarrollo de metodogías basadas en métodos formales.

La fecha de envío de artículos finaliza el 10 de Junio.