Temas

Temas de Razonamiento automático (2014-15)

• Tema 1: Programación funcional en Isabelle.
• Tema 2: Razonamiento sobre programas:
  • Tema 2a: Razonamiento sobre programas Haskell
  • Tema 2b: Razonamiento automático sobre programas en Isabelle/HOL.
• Tema 3: Razonamiento estructurado sobre programas en Isabelle/HOL.
• Tema 4: Razonamiento por casos y por inducción.
• Tema 5: Verificación de algoritmos de ordenación:
  • Tema 5a: Verificación de la ordenación por inserción.
  • Tema 5b: Verificación de la ordenación por mezcla.
• Tema 6: Caso de estudio: Compilación de expresiones.
• Tema 7: Deducción natural proposicional:
  • Tema 7a: Deducción natural proposicional].
  • Tema 7b: Deducción natural proposicional con Isabelle/HOL.
• Tema 8: Deducción natural de primer orden:
  • Tema 8a: Deducción natural en lógica de primer orden].
  • Tema 8b: Deducción natural en lógica de primer orden con Isabelle/HOL
• Tema 9: Conjuntos, funciones y relaciones.
• Tema 10: Conjuntos definidos inductivamente.
• Tema 11: Gramáticas libre de contexto.
• Tema 12: Misceláneas:
• Tema 12a: Razonamiento modular (Teoría de grupos).
• Tema 12b: Razonamiento modular.
• Tema 12c: Automatización.
• Tema 12d: Pasos elementales.
• Tema 12e: Sudoku.