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 Equipo: ANVA, JMHP, AVS, DCCG, FBV. Fecha de exposición: martes 26 de mayo. 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 Equipo: EV, LAGR, CUM, STF, KLB, BIST. Fecha de exposición: miércoles 20 de mayo. 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 Equipo: AGL, LVOR, SVC, DPT. Fecha de exposición: jueves 28 de mayo.
  • Lógicas temporales Equipo: JSV, JDM, NEAF, PAR, DMH. Fecha de exposición: viernes 22 de mayo. 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) Equipo: GEJC, ADGE, FTER, LRTF, RCR, NOGV. Fecha de exposición: lunes 25 de mayo. 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 Equipo: MEM, MDSM, OAJM, CECR, HHA, MAOD. Fecha de exposición: miércoles 27 de mayo.
  • 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.