Docencia: Lógica Informática 2021-22

• Anuncios (actualizado: 05/11/21)
  
• Ficha Técnica
• Contenido
• Sistemas
• Criterios de Evaluación
• Bibliografía

Ficha Técnica

Grado: Tecnologías Informáticas (Ingeniería en Informática)

Horario:

			L	M	X	J	V
G1	J.Borrego	I0.10		12:30-14:30	10:30-12:30
G2	F.Lara	F0.10			12:30-14:30		10:30-12:30
G3	F.Sancho	F0.10	15:30-17:30			17:30-19:30

Profesores: Joaquín Borrego Díaz, Félix Lara Martín, Fernando Sancho Caparrini

Tutorías: Consultar y acordar con el profesor del grupo correspondiente.

Contenido

La primera pregunta que puede hacerse cualquier alumno de Informática al comenzar esta asignatura es: ¿porqué debería un informático aprender Lógica?

Además de la labor de entrenamiento que supone aprender cualquier disciplina formal, podemos destacar, esencialmente, dos grandes vías para responder a esta pregunta:

1. En relación al modelado de tareas que se realiza con el objetivo de automatizarlas en un ordenador (una de los usos más habituales de los ordenadores hoy en día y de las labores de un informático), se debe tener en cuenta que esta automatización requiere del modelado de procesos que se realizan por humanos de formas muy distintas, y debemos ser capaces de realizar esta tarea de manera óptima (en lo que interviene la Lógica como modelador de tareas) y de verificar que el proceso implementado en el ordenador es correcto (donde la Lógica es insustituible).
2. Pero, además, hay aplicaciones específicas relacionadas con la computación en las que la Lógica juega un papel fundamental. Por ejemplo: Descripción de semántica de lenguajes de programación; Corrección de sistemas y protocolos informáticos; Descripción del hardware informático; Razonamiento Automático; Modelado de Sistemas Inteligentes; etc.

Por ello, y dentro de la amplísima gama de técnicas que podemos encontrar en la Lógica, el objetivo específico de esta asignatura es el de estudiar la representación del conocimiento mediante la Lógica Proposicional (LP) y la Lógica de Primer Orden (LPO), así como proponer métodos de razonamiento para cada una de ellas (como son los tableros semánticos y el método de resolución). En este sentido, el contenido del curso se ha dividido en las siguientes unidades temáticas:

Temas
Tema 0. Presentación - Recurso 0.1: Breve Historia de la Lógica - Recurso 0.2: Introducción a la Lógica
Tema 1: Sintaxis y Semántica de las Lógicas - Recurso 1.1: Sintaxis y Semántica LP - Recurso 1.2: Sistemas Deductivos Proposicionales - Recurso 1.3: Ejemplos resueltos formalización LP - Recurso 1.4: Sintáxis y Semántica LPO - Recurso 1.5: Ejemplos resueltos formalización LPO
Tema 2: Tableros Semánticos - Recurso 2.1: Tableros Semánticos en LP - Recurso 2.2: Tableros Semánticos en LPO - Recurso 2.3: Herramienta web de Tab. Sem. (LP y LPO)
Tema 3: Formas Normales y Algoritmo DPLL Herramienta para FNC y FND (entre otras)
Tema 4: Formas Prenex, de Skolem y Teorema de Herbrand
Tema 5: Resolución - Recurso 5.1: De la Resolución LP a la Resolución LPO - Recurso 5.2: Algunos ejercicios resueltos
Tema 6: Aplicaciones Introducción a Prover9 y Mace4 Problemas de Satisfacción de Restricciones Soluciones Problemas SAT (Touist)

Cada tema dispone de un conjunto de ejercicios propuestos que son de realización aconsejable para una correcta asimilación de los conceptos teóricos introducidos, así como de sus aplicaciones prácticas. Si las condiciones lo permiten, a lo largo del curso se destinarán algunas de las clases presenciales para la realización de ejercicios seleccionados y responder dudas que puedan haber surgido durante el desarrollo de los temas.

Sistemas

• LogicUS. 
• Prover9 y Mace4. Prover9 es un demostrador automático de teoremas para lógicas de primer orden (también puede ser usado para proposicional), y Mace4 busca modelos finitos y contraejemplos.
  • En esta entrada puedes encontrar un pequeño manual de uso y algunos ejemplos básicos de cómo aplicarlo en problemas de LP y LPO.
• TouIST: Un pequeño lenguaje de programación que permite expresar fórmulas proposicionales de una forma cómoda y natural.
• Algunas otras herramientas que pueden ser interesantes a lo largo del curso son:
  • Gateway to Logic: Permite realizar operaciones varias sobre fórmulas proposicionales (formas normales, tablas de verdad, árboles de formación, etc.).
  • ProofTools: Una aplicación para la generación automática y gráfica de Tableros Semánticos. Funciona, entre otras, para la LP, LPO y LPO con igualdad.
  • Tree Proof Generator: Genera Tableros Semánticos en LP y LPO.
  • LogEx: Convierte a formas normales y prueba equivalencias en LP. Se puede usar como herramienta de ejercicios porque permite la verificación de los pasos dados por el usuario, y también muestra la solución paso a paso. (Usa cualquier número como login).
  • Logica - Unifier: Aplica el algoritmo UMG a dos expresiones.
  • SATRennesPA: Verificador de SAT para LP.
  • Logictools: Un conjunto de librerías javascript para realizar diversos algoritmos (tablas de verdad, DPLL y resolución) para LP. El enlace lleva a una página preparado para probarlos.

Anuncios

Aquí se irán publicando anuncios relevantes relativos a la ejecución del curso (como, por ejemplo, las fechas acordadas para la realización de los exámenes de la evaluación alternativa para cada grupo):

• 20/12/21:
  • 2º Examen Parcial Grupo 1 - Doble Grado: Miércoles 12/01/2022, 10:20-12:20 en el aula I0.10.
• 05/11/21:
  • 2º Examen Parcial Grupo 1 - Grado TI: Miércoles 12/01/2022, 10:30-12:30 en el aula A2.16.
  • 2º Examen Parcial Grupo 2: Viernes 14/01/2022, 10:30-12:30.
  • 2º Examen Parcial Grupo 3: Jueves 13/01/2022, 17:30-19:30 en el aula H0.11.
• 04/11/21:
  • 1er Examen Parcial Grupo 1: Martes 30/11/2021, 12:30-14:30 en el aula A3.10.
  • 1er Examen Parcial Grupo 2: Miércoles 01/12/2021, 12:30-14:30 en el aula A1.16.
  • 1er Examen Parcial Grupo 3: Jueves 25/11/2021, 17:30-19:30 en el aula H0.11.
• 14/10/21: Se ha modificado la relación 1 de ejercicios para añadir un ejercicio más.
• Inicio del curso.

Criterios de Evaluación

Se proporcionan dos métodos (no excluyentes entre sí) de aprobar la asignatura:

• Evaluación alternativa: Realizando a lo largo del cuatrimestre dos pruebas escritas de carácter obligatorio, una correspondiente a los 3 primeros temas del curso (1 a 3), y otra a los temas restantes (4 a 6). La media aritmética de estos dos exámenes será la nota asociada a la evaluación alternativa, y su superación permitirá aprobar la asignatura sin necesidad de realizar el examen final. Las fechas de estas pruebas serán anunciadas con suficiente antelación en esta misma página, y se realizarán en horas lectivas del curso y en cada grupo por separado.
• Evaluación final: Mediante la superación de un examen final en las fechas previstas en el calendario de Organización Docente de la E.T.S.I.I.

Bibliografía

• Huth, M. y Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004.
• Ben-Ari, M.: Mathematical Logic for Computer Science. Prentice Hall, 1993.
• Davis, M.; Sigal, R.; Weyuker, E.: Computability, complexity and languages. Academic Press, 1994.
• Doets, K.: From Logic to Logic Programming. MIT Press, 1994
• Poole, D.; Mackworth, A.; Goebel, R.: Computational Intelligence. Oxford University Press, 1998.
• Russel, S.; Norvig, P.: Inteligencia Artificial. Un enfoque moderno. Pearson–Prentice Hall, 2003 (segunda edición).
• Alonso, J.A.; Borrego, J.: Deducción automática (Vol. 1: Construcción lógica de sistemas lógicos). Ed. Kronos, 2002.
• Nilsson, U.; Maluszynski, J.: Logic, Programming and Prolog. John Willey and Sons Ltd., 1990.