Ciencias de la Computación (plan 2013) 2024-2

Cuarto Semestre, Lógica Computacional

Si te interesa tomar la clase como oyente, eres bienvenidx. Sin embargo, bajo ninguna circunstancia se guardarán calificaciones o se "pasarán" a otrxs profesorxs.

✨ Contacto

La entrega de trabajos se realizará mediante la plataforma Google Classroom. Adicionalmente se tendrá un grupo de Telegram para tener una comunicación más fluida.

Los datos de acceso a las plataformas y medios de comunicación con el grupo serán enviados a su correo electrónico una vez completada su inscripción al curso. Revisen que su correo se encuentre actualizado en el sistema XFC.

🏅 Objetivos generales

El objetivo del curso es introducir las lógicas formales y sus aplicaciones en Ciencias de la Computación. En particular, se analizan los casos de la lógica proposicional y la lógica de primer orden, junto a sus métodos formales de deducción y demostración dando además especial énfasis a la implementació́n de estos métodos.

☝️ Requisitos

Se recomienda haber llevado (y preferentemente aprobado) las siguientes materias para aprovechar al máximo el curso:

• Estructuras Discretas
• Introducción a Ciencias de la Computación (saber programar)
• Estructuras de Datos

Cualquier duda sobre la inscripción y los requisitos se puede consultar en el correo manu@ciencias.unam.mx.

💯 Evaluación

Exámenes parciales 30%

Se aplicarán un total de cuatro exámenes parciales que evaluarán una cuarta parte del curso respectivamente. Los exámenes incluirán principalmente problemas que se resuelvan usando los conceptos teóricos estudiados en el curso. Los exámenes se presentarán de forma individual. En caso de no poder presentar alguno de los exámenes en la fecha correspondiente, se tendrá una ronda de reposiciones y dos de finales.

Evaluaciones semanales 20%

Al final de cada semana, los días viernes, se realizarán pequeñas evaluaciones que permitirán medir el avance del grupo. Estas evaluaciones pueden consistir en preguntas conceptuales, ejecución de algoritmos, dinámicas en equipo, entre otras. El número de integrantes se definirá en función del tipo de evaluación.

Proyecto final 30%

Se asignará un proyecto final de investigación cuya solución requiera de una implementación poniendo en práctica los conocimientos adquiridos a lo largo del semestre. El proyecto incluirá la redacción de un reporte y la codificación de la solución usando el lenguaje de programación Haskell, el lenguaje de programación Prolog o el asistente de pruebas Coq, que se estudiarán a lo largo del curso en las sesiones de laboratorio. La solución del proyecto deberá presentarse ya sea mediante una exposición o mediante un vídeo, la forma de presentarlo se definirá cuando esté cerca su entrega y de acuerdo al avance del grupo.

Prácticas 20%

Se dejarán prácticas de laboratorio quincenales cuyo objetivo será implementar los algoritmos y técnicas estudiadas a lo largo del curso. Las implementaciones se realizarán en Haskell, Prolog y Coq. Las prácticas podrán entregarse en equipos de máximo 3 integrantes. Se podrán entregar prácticas a destiempo pero se tendrá una penalización de un punto por cada día de retraso.

📚 Contenido

Unidad 01: Introducción

• 1.1. ¿Qué es la Lógica Computacional?
• 1.2. Aplicaciones en Ciencias de la Computación
• 1.3. Sistemas lógicos y sus propiedades
• 1.4. Caso de estudio 01: Diseño de circuitos lógicos

Unidad 02: Lógica proposicional

• 2.1. Sintaxis
• 2.2. Semántica
• 2.3. Equivalencia lógica
• 2.4. Análisis de argumentos correctos
• 2.5. Resolución binaria
• 2.6. El problema SAT
• 2.7. Caso de estudio 02: El problema de las 8 reinas

Unidad 03: Lógica de predicados

• 3.1. Sintaxis
• 3.2. Semántica
• 3.3. Equivalencia lógica
• 3.4. Análisis de argumentos correctos
• 3.5. Resolución binaria con unificación
• 3.6. Programación lógica
• 3.7. Caso de estudio 03: Algoritmo de Wang

Unidad 04: Introducción a la verificación formal

• 4.1. Razonamiento ecuacional
• 4.2. Cálculo de secuentes
• 4.3. El asistente de pruebas Coq
• 4.4. Pruebas por inducción
• 4.5. Listas y polimorfismo
• 4.6. Tácticas
• 4.7. Lógica en Coq
• 4.8. Proposiciones definidas inductivamente
• 4.9. La correspondencia de Curry-Howard
• 4.10. Caso de estudio 04: Ordenamiento por inserción

🛠️Herramientas y tecnologías a utilizar

• Lenguaje de programación Haskell + MiniSAT
• Lenguaje de programación Prolog
• Asistente de pruebas Coq

📖Bibliografía

[1] Huth M., Ryan M. Logic in Computer Science, modelling and reasoning about systems. 2nd Edition, Cambridge University Press 2004.

[2] Ben-Ari M. Mathematical Logic for Computer Science. 2nd Edition, 3rd corrected printing. Springer 2008.

[3] Favio E. Miranda, A. Liliana Reyes, et.al. Notas de Clase del Curso de Lógica Computacional, Facultad de Ciencias UNAM, Revisión 2022-1.

[4] José L. Fernández, Ángeles Manjarrés, et.al. Lógica Computacional, Apuntes de Clase, UNED, 2007.

[5] Miran Lipovaca, Learn you a Haskell for great good: A beginner’s guide, No Starch Press, Primera edición, 2011.

[6] Graham Hutton, Programming in Haskell, Cambridge University Press, Segunda edición, 2016.

[7] Ulle Endriss, Introduction to Prolog Progamming, Universiteit Van Amsterdam, 2018.

[8] William Clocksin, Programming in Prolog using the ISO Standard, Springer, Primera edición, 2003.

[9] Pierce, B. C., Casinghino, C., et. al., Software foundations, 2021.