Presentación del Seminario de Algorítmica, Matemáticas y Programación

PorJosé A. Alonso

En el seminario de hoy del GAMPUS (Grupo de Algorítmica, Matemáticas y Programación de la US) se ha comentado:

  • Los objetivos del Seminario: el desarrolllo de la habilidad de resolver problemas computacionales como los propuestos en las competiciones de programación.
  • El sistema Kattis que se usará como plataforma para la propuesta de las competiciones y su evaluación.
  • La forma de registrarse en Kattis.
  • Los lenguajes de programación aceptados por Kattis.
  • La forma de subir las soluciones de problemas a Kattis.
  • Un ejemplo de publicación en la Wiki de las solucionas subidas a Kattis ordenadas por tiempo y lenguaje del problema A different problem.
  • La metodología del Seminario: semanalmente se propondrá una competición en Kattis. Además, para cada problema se creará una página en la Wiki para escribir las soluciones como en el ejemplo anterior.
  • Las referencias útiles para el Seminario.
  • Algunos cursos relacionados con el Seminario.

Como referencia de lo tratado se puede usar el primer capítulo del libro Principles of algorithmic problem solving de Johan Sannemo.

Para la próxima semana se ha propuesto la primera competición.

RA2018: Presentación del curso de “Razonamiento automático”

PorJosé A. Alonso

En la clase de hoy del curso Razonamiento automático se ha hecho una presentación del mismo, comentando los siguientes puntos

  1. Objetivo: El objetivo fundamental del curso es la verificación de programas y de demostraciones matemáticas. Su necesidad se basa en la seguridad de sistemas críticos, en los teoremas incompletos y en los teoremas enormes (como el teorema de los 4 colores). Una colección de ejemplos de verificación se encuentra en The Archive of Formal Proofs.

  2. Sistema: Los sistemas que se usarán son Isabelle/HOL y Coq.

  3. Punto de partida: El punto de partida es el conocimiento de la programación funcional con Haskell (correspondiente a los 10 primeros temas del curso de informática y de la deducción natural (correspondiente a los temas 2 y 8 del curso de Lógica informática.

  4. Metodología: El curso será esencialmente práctico con relaciones semanales de ejercicio. El material del curso se irá publicando en la página del curso, en la se pondrá los

    • temas (con las teorías de cada tema),
    • ejercicios (con los relaciones de ejercicios),
    • documentación (con enlaces a lecturas recomendadas),
    • sistemas (con enlaces a los sistemas utilizados) y
    • diario (con el resumen de cada clase).

Las dos referencias fundamentales, para la parte de Isabelle/HOL, son los apuntes Programming and proving in Isabelle/HOL y el libro A proof assistant for higher-order logic.

Como tareas para la próxima clase se propusieron: