SLEAM

Después de 4 meses, reanudo la escritura en Vestigium. Como uno de sus objetivos era servir de diario de las publicaciones en mi sitio en la Red, voy a resumir las realizadas desde la anterior entrada en Vestigium.

He publicado una introducción al sistema de cálculo simbólico Maxima que he usado en las asignaturas de I1M (Informática de 1º de Matemáticas) como en la de SLEAM (Sofware libre para la enseñanza y aprendizaje de las Matemáticas). Los temas y ejercicios publicados son los siguientes:

• Tema 14: Introducción a Maxima.
• Tema 15: Funciones de una variable.
• Tema 16: Aritmética.
• Tema 17: Sucesiones y recursión.
• Tema 18: Programación.
• Tema 19: Matrices en Maxima.
• Tema 20: Gráficos y animaciones.

las relaciones de ejercicios:

• Relación 24.
• Relación 25.
• Relación 26.

Además, en I1M (Informática de 1º de Matemáticas) he publicado dos nuevos temas sobre diseño de algoritmos con Haskell:

• Tema 21: Algoritmos de exploración de grafos.
• Tema 22: Tipos de datos: Polinomios.

En la página de publicaciones he añadido las dos más recientes:

• A logic approach to decision taking in a railway interlocking system using Maple. Mathematics and Computers in Simulation (En colaboración con E. Roanes, A. Hernando y L.M. Laita).
• Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2. Journal of Automated Reasoning. (En colaboración con F.J. Martín, J.L. Ruiz y M.J. Hidalgo).

Finalmente, en la wiki del Grupo de Lógica Computacional he añadido las formalizaciones de teorías en PVS:

• A Formalization of Abstract Properties of Confluent Reductions in PVS.
• Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO).
• A formally verified prover for the ALC description logic (in PVS).
• Verification of the formal concept analysis in PVS.
• A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution.
• Theory of Refinements in PVS.