Docencia: Lógica Informática 2017-2018

Modificado el 21 de Noviembre de 2017

Ficha Técnica

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

Horario:

G1 F. Sancho A2.14 Martes (08:30 - 10:20) Jueves (10:40 - 12:30)
G2 F. Lara A2.11 Martes (10:40 - 12:30) Jueves (12:40 - 14:30)
G3 F. Sancho H1.12 Martes (15:30 - 17:20) Jueves (17:40 - 19:30)

Profesores: Félix Lara MartínFernando Sancho Caparrini

Tutorías: Consultar 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:

 
Tema I: Sintaxis y Semántica de LP y LPO
Tema II: Formas Normales y Prenexas
Tema III: Tableros Semánticos para LP y LPO
Tema IV: Algoritmo DPLL y Teorema de Herbrand
Tema V: Sistemas Deductivos en LP y Resolución en LP y LPO

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 de los Grupos G1 (en el aula H1.10), G2 (en el aula I1.10) y G3 (en el aula H1.12) será el día Martes, 28 de Noviembre en la hora de clase.
  • El día Jueves, 30 de Noviembre, los grupos G1 y G3 no tendrán 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 (50% de la calificación), y otra a los temas restantes (50% de la calificación). La superación de estas pruebas 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.