{"id":5562,"date":"2016-10-20T13:40:08","date_gmt":"2016-10-20T11:40:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5562"},"modified":"2016-10-20T13:40:08","modified_gmt":"2016-10-20T11:40:08","slug":"ra2016-presentacion-del-curso","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2016-presentacion-del-curso\/","title":{"rendered":"RA2016: Presentaci\u00f3n del curso"},"content":{"rendered":"

En la clase de hoy del curso Razonamiento autom\u00e1tico<\/a> se ha hecho una presentaci\u00f3n del mismo, comentando los siguientes puntos<\/p>\n

    \n
  1. Objetivo<\/strong>: El objetivo fundamental del curso es la verificaci\u00f3n de programas y de demostraciones matem\u00e1ticas. Su necesidad se basa en la seguridad de sistemas cr\u00edticos<\/a>, en los teoremas incompletos<\/a> y en los teoremas enormes<\/a> (como el teorema de los 4 colores<\/a>). Una colecci\u00f3n de ejemplos de verificaci\u00f3n se encuentra en The Archive of Formal Proofs<\/a>.<\/p>\n<\/li>\n
  2. \n

    Sistema<\/strong>: El sistema que se usar\u00e1 es Isabelle\/HOL<\/a>.<\/p>\n<\/li>\n

  3. \n

    Punto de partida<\/strong>: El punto de partida es el conocimiento de la programaci\u00f3n funcional con Haskell (correspondiente a los 10 primeros temas del curso de inform\u00e1tica<\/a>) y de la deducci\u00f3n natural (correspondiente a los temas 2 y 8 del curso de L\u00f3gica inform\u00e1tica<\/a>).<\/p>\n<\/li>\n

  4. \n

    Metodolog\u00eda<\/strong>: El curso ser\u00e1 esencialmente pr\u00e1ctico con relaciones semanales de ejercicio. El material del curso se ir\u00e1 publicando en la p\u00e1gina del curso<\/a>, en la se pondr\u00e1 los<\/p>\n