Docencia: Lógica Informática 2018-19

Modificado el 8 de Diciembre de 2018

Ficha Técnica

Grado: Ingeniería de Tecnologías Informáticas

Horario:

L M X J V
G1 F. Lara A2.14     8:30-10:20 10:40-12:30  
G2 F. Sancho A1.14     10:40-12:30 12:40-14:30  
G3 F. Sancho H1.12     15:30-17:20   17:40-19:30

Profesores: Félix Lara MartínFernando Sancho Caparrini

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

Contenido

El objetivo específico de la asignatura es 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 1: Sintaxis y Semántica de las Lógicas Proposicional y de Primer Orden
Tema 2: Tableros Semánticos
Tema 3: Formas Normales y Algoritmo DPLL
Tema 4:  Formas Prenex, de Skolem y Teorema de Herbrand
Tema 5: Sistemas Deductivos Proposicionales y Resolución
De la Resolución Proposicional a LPO
Tema 6: Aplicaciones

Cada tema dispone de un conjunto de ejercicios propuestos que son de realización indispensable para una correcta asimilación de los conceptos teóricos introducidos, así como de sus aplicaciones prácticas. 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 la resolución de los ejercicios del tema en curso.

Sistemas

  • Prover9 y Mace4Prover9 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.
  • 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.).
    • 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.
    • DPLL Algorithm Demo: Una demostración de cómo funciona DPLL representándolo por medio de grafos (no es exactamente igual que como lo representamos en clase).
    • 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.
    • d3-dpll: Una sencilla implementación de DPLL con ejecución paso a paso.

Anuncios

Aquí se irán publicando anuncios relevamtes 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).

  • El primer examen parcial será, por grupos, y durante las horas de clase:
    • G1: Jueves, 29 de Noviembre de 2018 (Aula I1.10).
    • G2: Jueves, 22 de Noviembre de 2018 (Aula H0.13).
    • G3: Viernes, 23 de Noviembre de 2018 (Aula H1.12).
  • Calificaciones del Primer Examen Parcial de los Grupos 2 y 3 (juntos). Recuerda que has de usar la clave dada en clase.

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, y otra a los temas restantes. 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.