Dentro del marco del ITP’01 se va a celebrar el PAR-2010: Workshop on Partiality and Recursion in Interactive Theorem Provers.
Uno de los temas del congreso es la automatización de las demotraciones de terminación de funciones. Sobre este tema hemos trabajado en nuestro grupo tanto en ACL2 como en PVS.
El congreso se celebrará el 15 de Julio en Edimburgo. El plazo de envío de artículos termina el 19 de marzo.
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
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).
Hoy he publicado la relación 14 de ejercicios de Informática de 1º de Matemáticas.
Contiene 5 ejercicios del proyecto Euler.
A lo largo de la semana los alumnos escribirán las soluciones de la relación 14.
Hoy publica “El País” el artículo España, blanco de más de cuarenta ciberataques. El artículo es un reportaje sobre “la guerra de los ciberespías” a raíz del ataque a Google. Además cuenta las iniciativas españolas para aumentar la seguridad.
Desde sus inicios los métodos formales se han aplicado a aumentar la seguridad de los sistemas críticos y, más generalmente, a la ingeniería de la seguridad. Dado el uso de la Red, sus programas y servicios se están convirtiendo en sistemas críticos y, por tanto, en campo de aplicación de los métodos formales. Muestra del interés de los sistemas de Red para los métodos formales son la realización de tesis como las siguientes
Read More “Métodos formales y seguridad en la Red”
Un indicador de la vitalidad de un área lo constituye los números especiales de revistas dedicadas al área.
La revista Mathematical Structures in Computer Science ha anunciado un número especial sobre Advances and Perspectives in the Mechanization of Mathematics.
En el anuncio se constata el éxito obtenido formalizando algunos teoremas matemáticos importantes tales como el teorema de los números primos, el teorema de los cuatro colores y el teorema de la curva de Jordan.
El número desea reflejar los avances recientes y las nuevas perspectivas dentro del campo de la formalización del conocimiento matemático, incluyendo descripciones de nuevas formalizaciones.
La fecha límite para el envío de artículos es el 28 de Junio de 2010.