Temas para las exposiciones

La evaluación de la última parte del curso será mediante exposiciones, cuyos temas a elegir se muestran a continuación. Los equipos deben ser de cinco o seis integrantes. En breve, manden un correo a indicando los miembros del equipo y dos temas en los que están interesados, le daré prioridad al primer tema pero si ya está asignado tomaré en cuenta el segundo.

Lo que espero es una explicación a manera de introducción de cada uno de los temas, que sea didáctica, con imágenes, cuestionarios (por ejemplo, kahoot), ejecuciones de software según sea el caso, ejemplos y aplicaciones. No olviden proporcionar la bibliografía de donde sacaron el material de la exposición. El tiempo será de no más de 50 minutos, y 10 minutos para responder preguntas.

  • Problema SAT Cubrir:
    • Marques-Silva, J. Practical applications of boolean satisfiability. 2008 9th International Workshop on Discrete Event Systems 74–80 (2008).
    • Horbach, A., Bartsch, T. & Briskorn, D. Using a sat-solver to schedule sports leagues. J. Sched. 15, 117–125 (2012).
    • Rintanen, J. Planning with specialized sat solvers. Proc. AAAI Conf. Artif. Intell. 25, 1563–1566 (2011).
  • La no decibilidad de la lógica de predicados Cubrir:
    • Sección 2.3 Undecidability de Schöning, U., Logic for Computer Science. Progress in Computer Science and Applied Logic v.8, 1989.
  • Isomorfismo de Curry-Howard
  • Lógicas temporales Cubrir:
    • Huth M., Ryan M. Logic in Computer Science, modelling and reasoning about systems. Capítulo: 3. Verification by model checking.
    • Dar ejemplos concretos y prácticos de lo que se puede expresar en lógica temporal y las propiedades que se demuestran con este formalismo.
  • Binary Decision Diagrams (BDDs) Cubrir:
    • Huth M., Ryan M. Logic in Computer Science, modelling and reasoning about systems. Capítulo: 6. Binary decision diagrams.
    • Mostrar varios diagramas de BDDs ilustrando las operaciones sobre ellos.
  • Lógicas de orden superior
  • Asistente de pruebas COQ
  • Verificación formal mediante Isabelle

Mantendré actualizado este sitio para que observen los temas que ya fueron asignados y los que siguen disponibles.