UNIVERSIDAD NACIONAL AUTÓNOMA DE MÉXICO
Licenciatura en Ciencias de la Computación
Facultad de Ciencias
Programa de la asignatura
Denominación de la asignatura:
Lógica Computacional
Clave: Semestre: Eje temático: No. Créditos:
4 Estructuras Discretas 10
Horas por Total de
Carácter: Obligatoria Horas
semana Horas
Teoría: Práctica:
Tipo: Teórico-Práctica
4 2 6 96
Modalidad: Curso Duración del programa: Semestral
Asignatura con seriación obligatoria antecedente: Álgebra Superior I;Estructuras Discretas
Asignatura con seriación obligatoria subsecuente: Complejidad Computacional
Asignatura con seriación indicativa antecedente: Álgebra Superior II
Asignatura con seriación indicativa subsecuente: Lenguajes de Programación; Inteligencia
Artificial
Objetivo general:
Concer y aplicar la lógica como una herramienta formal de apoyo en diversas áreas de las
ciencias de la computación.
Índice temático
Horas
Unidad Temas
Teóricas Prácticas
I Introducción 2 2
II Lógica proposicional 7 10
III Lógica de predicados de primer orden 8 10
IV Análisis de argumentos 6 8
V Sistemas deductivos 9 12
VI El paradigma de programación lógica 10 14
VII Extensiones y aplicaciones (opcional) 6 8
Total de horas: 48 64
Suma total de horas: 112
72
Contenido temático
Unidad Tema
I Introducción
I.1 Importancia de la lógica para las ciencias computacionales.
I.2 Panorama de aplicaciones en distintas áreas de las ciencias de la computación.
II Lógica proposicional
II.1 Sintaxis: lenguaje formal, recursión e inducción estructural.
II.2 Sustitución textual.
II.3 Semántica: funciones de interpretación.
II.4 Decidibilidad de la lógica proposicional.
II.5 Análisis de argumentos lógicos: interpretaciones y/o tableaux semánticos (reglas
y ).
II.6 Resolución binaria: formas normales negativa y conjuntiva, resolución binaria
proposicional, algoritmos de saturación, el problema SAT.
III Lógica de predicados de primer orden
III.1 Sintaxis y ejemplos de especificación formal.
III.2 Conceptos sintácticos: recursión e inducción estructural en términos y fórmulas,
ligado de variables.
Sustitución: el problema de la sustitución textual y la captura de variables libres,
III.3
definición y -equivalencia, definición formal de sustitución.
III.4 Semántica: introducción; interpretación de términos y fórmulas; definición de
satisfacción de Tarski.
III.5 Conceptos semánticos: verdad, modelos, validez y equivalencia lógica.
IV Análisis de argumentos
IV.1 La noción de consecuencia lógica.
IV.2 Argumentos incorrectos: construcción de modelos contraejemplo.
IV.3 El teorema de indecidibilidad de Church.
V Sistemas deductivos
V.1 Generalidades: reglas de inferencia; correctud, completud y completud refutacional.
V.2 Tableaux semánticos: reglas y
V.3 Deducción natural: uso de contextos; lógica minimal, intuicionista y clásica; el
teorema de completud de Gödel.
V.4 Formas normales: prenex, de Skolem, forma clausular.
Resolución binaria: cláusulas cerradas; unificación: unificadores más generales,
V.5 algoritmo de Martelli-Montanari; algoritmos de saturación; estrategias de derivación
(resolución lineal, resolución unitaria, conjunto de soporte).
VI El paradigma de programación lógica
VI.1 Resolución SLD: cláusulas de Horn y programas lógicos.
VI.2 Semántica operacional y declarativa; modelos de Herbrand.
VI.3 El lenguaje de programación Prolog: aritmética, listas, árboles, el operador de
corte.
VII Extensiones y aplicaciones (opcional a elegir alguno de los siguientes temas u otro
relacionado a criterio del profesor)
VII.1 Introducción a los sistemas de tipos; la correspondencia de Curry-Howard.
73
VII.2 Lógicas no clásicas: modal, temporal, de Hoare, dinámica, etcétera.
VII.3 Lógicas de orden superior: lógica de segundo orden, lógicas relacionales
Bibliografía básica:
1. Huth M., Ryan M. Logic in Computer Science, modelling and reasoning about systems. 2nd
Edition, Cambridge University Press 2004.
2. Nerode A., Shore R.A. Logic for Applications. 2nd. Edition. Graduate Texts in Computer
Science. Springer 1997.
Bibliografía complementaria:
1. Ben-Ari M. Mathematical Logic for Computer Science. 2nd Edition, 3rd corrected printing.
Springer 2008.
2. Fitting M., First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer
Science. 2nd. Edition. Springer 1996.
3. Sperschneider V., Antoniou G. Logic, A Foundation for Computer Science. Addison-Wesley
1991.
4. Socher-Ambrosius R., Johann P. Deduction Systems. Graduate Texts in Computer Science.
Springer 1997.
Sugerencias didácticas: Métodos de evaluación:
Exposición oral (X) Exámenes parciales (X)
Exposición audiovisual ( ) Examen final escrito (X)
Ejercicios dentro de clase (X) Trabajos y tareas fuera del aula (X)
Ejercicios fuera del aula (X) Exposición de seminarios por los alumnos ( )
Seminarios ( ) Participación en clase (X)
Lecturas obligatorias (X) Asistencia ( )
Trabajo de investigación ( ) Seminario ( )
Prácticas de taller o laboratorio
(X)
Prácticas de campo ( ) Otras: Prácticas de laboratorio. Proyectos de
programación.
Otras: __________________________
Perfil profesiográfico:
Egresado preferentemente de la Licenciatura en Ciencias de la Computación o Matemático con
especialidad en Computación. Es conveniente que posea un posgrado en la disciplina. Con
experiencia docente.
74
