Docencia: Lógica Informática 2018-19

Modificado el 15 de Octubre 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
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).

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.