{"id":3775,"date":"2013-10-24T19:26:32","date_gmt":"2013-10-24T17:26:32","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3775"},"modified":"2016-10-16T08:43:21","modified_gmt":"2016-10-16T06:43:21","slug":"ra2013-presentacion-del-curso","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2013-presentacion-del-curso\/","title":{"rendered":"RA2013: 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<\/b>: 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> y en los teoremas enormes<\/i> (como el teorema de los 4 colores<\/a>). Una colecci\u00f3n de ejemplos de verificaci\u00f3n se encuentra en el AFP<\/a>.<\/li>\n
  2. Sistema<\/b>: El sistema que se usar\u00e1 es Isabelle\/HOL<\/a>.<\/li>\n
  3. Punto de partida<\/b>: 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>).<\/li>\n
  4. Metodolog\u00eda<\/b>: 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\n