Wave equation numerical resolution: a comprehensive mechanized proof of a C program

Se ha publicado un nuevo artículo de formalización en Coq: Wave equation numerical resolution: a comprehensive mechanized proof of a C program.

Sus autores son Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond y Pierre Weis.

El resumen del artículo es

We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both method error and round-off error. We use Frama-C to generate theorems that guarantee the soundness of the code. We discharge these theorems using SMT solvers, Gappa, and Coq. This involves a large Coq development to prove the adequacy of the C program to the numerical scheme and to bound errors. To our knowledge, this is the first time such a numerical analysis program is fully machine-checked.

El código correspondiente se encuentra en http://fost.saclay.inria.fr/wave_total_error.html

El método de Pólya para resolver problemas

George Pólya presentó en su libro Cómo plantear y resolver problemas (en inglés, How to solve it) un método de 4 pasos para resolver problemas matemáticos. Dicho método fue adaptado para resolver problemas de programación, por Simon Thompson en How to program it.

En la siguientes secciones mostramos los 4 pasos de ambos métodos, junto con sus correspondientes preguntas.
Read More “El método de Pólya para resolver problemas”

LMF2012: Sustituciones en la lógica de primer orden

En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la sustituciones en la lógica de primer orden. Concretamente, se ha definido el concepto de sustitución y cómo se aplica a términos y fórmulas. Finalmente, se ha comentado que hay sustituciones que aplicadas a una fórmula satisfacible puede dar una fórmula insatisfacible. Esto motiva la definición de las sustituciones libres.

Las transparencias de esta clase son las páginas 1 a 8 del tema 7.

LMF2012: Semántica de la lógica de primer orden (2)

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se ha continuado la presentación de la semántica de la lógica de primer orden, extendiendo los conceptos semánticos de las fórmulas a los conjuntos. Concretamente, se ha definido los siguientes conceptos:

  • realizaciones y modelos de conjuntos de fórmulas,
  • conjuntos consistentes e inconsistentes,
  • consecuencia lógica y
  • fórmulas equivalentes.

También se ha estudiado las relaciones entre dichos conceptos

Las transparencias de esta clase son las páginas 39 a 45 del tema 6.