|
|
 |
|
MÉTODOS LÓGICOS: AUTOMATIZACIÓN DEL RAZONAMIENTO
Profesorado
| Coordinador: José Luis Fernández Vindel (Dpto. Inteligencia Artificial,
UNED) |
| Profesores: |
| Juan Heguiabehere (Universidad de Buenos Aires) |
|
|
|
|
Ficha técnica:
| Tipo | Optativa |
|
| Cuatrimestre | Primero |
| Créditos/horas totales | 6/150 |
| Horas de estudio teórico | 50 |
| Horas de prácticas | 50 |
| Horas complementarias | 50 |
DESCRIPCIÓN DE LA ASIGNATURA
Prerrequisitos recomendables
Ninguno diferente de los generales de acceso a este programa de postgrado
orientado a la investigación.
Objetivos generales de la materia
Evaluación del uso de sistemas lógicos como soporte de la inferencia
deductiva en IA: lógicas de primer orden, modales, temporales y descriptivas.
Claves para la automatización de estos sistemas. Uso de entornos lógicos
y probadores automáticos.
Breve reflexión sobre las limitaciones de estos sistemas en la resolución
de tareas de IA. Enumeración de alternativas no cubiertas: inferencia
no monótona, inductiva y abductiva, manejo de incertidumbre, etc.
Destrezas y competencias
-(Sobre Sintaxis) Reconocer cómo se define formalmente la sintaxis
de un sistema lógico. Desarrollar la habilidad de comparación crítica
entre los lenguajes propuestos.
-(Sobre Sintaxis) Ser capaz de implementar la generación y análisis
sintáctico de estos lenguajes.
-(Sobre Semántica) Reconocer cómo se define la semántica asociada
a un lenguaje lógico. Desarrollar la capacidad de comparación formal
entre semánticas: uso de la traducción o simulación formal entre sistemas,
análisis de la expresividad.
-(Sobre Semántica) Ser capaz de implementar la comprobación de un
modelo para fórmulas sencillas y modelos finitos simples. Reconocer
los fundamentos teóricos, las limitaciones y la elección de estrategias
en generadores y comprobadores de modelos.
-(Sobre Inferencia) Consolidar el uso correcto de los diversos sistemas
de inferencia propuestos para cada lógica presentada. Reutilizar el
conocimiento y experiencia sobre un sistema deductivo para afrontar
otro similar: p.ej., a lo largo de los sistemas de tableaux propuestos
para cada lógica. Aprender a generar demostraciones y pruebas en un
sistema inferencial a partir de otras en otro sistema. Preguntarse
por las propiedades de cada sistema lógico: corrección, completud,
decidibilidad...
-(Sobre Inferencia) Conocer las propuestas básicas de implementación
de los sistemas inferenciales más usados: resolución, tableaux, ...
y generar la habilidad de adaptarlos. Manejar probadores de teoremas
basados en estos métodos. Ser consciente del grado de complejidad
computacional de las tareas inferenciales.
-(Aplicabilidad) Desarrollar la capacidad formal de uso efectivo de
estos sistemas: planteamiento de tareas y problemas representables
en estas lógicas, cuya resolución se alcance mediante la resolución
de alguno de los servicios inferenciales del sistema lógico utilizado.
-(Aplicabilidad) Desarrollar la capacidad práctica de uso de estos
sistemas lógicos mediante la adaptación y composición de herramientas
ya disponibles. Saber precisar sus limitaciones.
Contextualización de la materia en el conjunto del Master
Esta asignatura se encuadra en el Master "Inteligencia Artificial
Avanzada: Fundamentos, Métodos y Aplicaciones", y se presenta
como optativa en la Especialidad "Sistemas Inteligentes de
Diagnóstico, Planificación y Control".
En ella se facilitan algunos sistemas lógicos como métodos de resolución
de tareas en IA. Es cierto que gran parte del estudio se centra en
la definición, uso correcto e implementación de estos sistemas; sin
embargo, se potenciará finalmente su percepción como métodos utilizables
para el desarrollo del trabajo final del Máster (cualquiera que éste
sea).
Tan sólo se sugieren, como conocimiento previo, los que se presentan
usualmente sobre Lógica Proposicional y de Primer Orden en los estudios
superiores de Informática. Esta revisión previa se contempla también
como asignatura optativa del Master, dentro de un bloque adicional
de 60 créditos que no se oferta en esta convocatoria 2006-07.
1 Medios de estudio
1.1 Metodología docente
La general del programa de postgrado. Junto a las actividades y enlaces
con fuentes de información externas, existe material didáctico propio
preparado por el equipo docente.
Adaptada a las directrices del EEES, de acuerdo con el documento del
IUED.
La asignatura no tiene clases presenciales. Los contenidos teóricos
se impartirán a distancia, de acuerdo con las normas y estructuras
de soporte telemático de la enseñanza en la UNED.
El material docente incluye un resumen de los contenidos de cada tema
y distintos tipos de actividades relacionadas con la consulta bibliográfica
y la utilización de herramientas asociadas a las tecnologías y técnicas
presentadas en el curso.
Tratándose de un máster orientado a la investigación, las actividades
de aprendizaje se estructuran en torno al estado del arte en cada
una de las materias del curso y a los problemas en los que se va a
focalizar la práctica que el alumno deberá realizar.
1.2 Material de estudio
Se facilitarán materiales propios, accesibles por Red, y enlaces a
documentación no restringida publicada en Web.
Adicionalmente, el alumno dispone del acceso en línea al texto de
artículos, a través de las suscripciones de la Biblioteca de la UNED.
Los contenidos del curso, teóricos o aplicados, pueden encontrarse
en la siguiente relación resumida de textos.
Bibliografía Básica
-Nerode, A. y Shore R. A.; Logic for Applications, 2nd Edition. Springer,
2005.
-Huth, M. y Ryan M.; Logic in Computer Science, 2nd Edition. Cambridge
University Press, 2004.
-Baader, F.; The Description Logic Handbook, Cambridge University
Press, 2003.
-Brachman, R. y Levesque, H.; Knowledge Representation and Reasoning,
Morgan Kaufmann 2004.
1.3 Materiales y recursos de apoyo
La plataforma de e-Learning Alf, proporcionará el adecuado interfaz
de interacción entre el alumno y sus profesores. aLF es una plataforma
de e-Learning y colaboración que permite impartir y recibir formación,
gestionar y compartir documentos, crear y participar en comunidades
temáticas, así como realizar proyectos online.
Se ofrecerán las herramientas necesarias para que, tanto el equipo
docente como el alumnado, encuentren la manera de compaginar tanto
el trabajo individual como el aprendizaje cooperativo.
1.4 BIbliografia general de consulta
(No se vuelven a incluir las referencias de la bibliografía básica)
* Fundamentos teóricos de Lógica de Primer Orden
[1] The essence of Logic. John Kelly; 1997, Pearson Education
[2] Logic for Mathematics and Computer Science. Stanley N. Burris;
1998, Prentice-Hall
[3] Logic and Structure. Dirk van Dalen; 3rd edition 1997, Springer
[4] Introduction to Mathematical Logic. Elliot Mendelson; 4th edition,
1997 Chapman & Hall / CRC
* Automatización del razonamiento (Primer Orden)
[5] Propositional Logic: Deduction and Algorithms. Kleine Büning
& Lettmann; 1999, Cambridge University Press
[6] Logic for Computer Scientists. Uwe Schöning. 2001, Birkhäuser
[7] First-Order Logic and Automated Theorem Proving. Melvin Fitting:
2nd edition 1996, Springer
[8] Automated Theorem Proving: Theory and Practice. Monty Newborn;
2001, Springer
[9] A Fascinating Country in the World of Computing: your Guide
to Automated Reasoning. Larry Wos, Gail W. Pieper; 1999, World Scientific
Publishing
* Programación lógica
[10] From Logic to Logic Programming. K. Doets; 1994, MIT Press
[11] Programming in Prolog. W. F. Clocksin, C. S. Mellish; 4th edition,
1994 Springer
* Lógicas modales y temporales
[12] First Steps in Modal Logic. S. Popkorn; 1994, Cambridge University
Press
[13] Modal Logic. P. Blackburn, M. de Rijke, Y. Venema; 2001, Cambridge
University Press
[14] Epistemic Logic for AI and Computer Science. J.-J. Ch. Meyer,
W. v.d. Hoek; 1995, Cambridge University Press
[15] Model Checking. E. M. Clarke, O. Grumberg, D. A. Peled; 1999,
MIT Press
* Recopilaciones extensas (teoría y automatización)
[16] Handbook of Logic in Artificial Intelligence and Logic Programming.
D. M. Gabbay, C. J. Hogger, J. A. Robinson; 1993 Oxford Science Publications
[17] Handbook of Automated Reasoning. A. Robinson, A. Voronkov;
2001 Elsevier Science
[18] Handbook of Tableau Methods. M. D'Agostino, D. M. Gabbay; 2006
Springer
[19] Handbook of Modal Logic. P. Blackburn, J. v. Benthem, F. Wolter
(editors); 2006 Elsevier
1.5 Tutorización
La tutorización de los alumnos se llevará a cabo a través de la plataforma
de e-Learning Alf, por teléfono (913987181) y por correo electrónico
(jlvindel@dia.uned.es)
2 Estructura del curso
2.1 Estructura y contenido teórico
Tema 1: Lógica Proposicional
Tema 2: Lógica de Primer Orden
Tema 3: Lógicas Modales
Tema 4: Lógicas Temporales
Tema 5: Lógicas Descriptivas
Tema 6: Revisión, limitaciones y alternativas
2.2 Objetivos por tema y orientaciones breves
Tema 1: Lógicas Proposicionales
Objetivos:
(Teóricos) Fijar el conocimiento previo sobre el sistema, repasando
los conceptos semánticos básicos y sus interrelaciones. Se presentan
varios sistemas deductivos, entre los que se prestará atención especial
a los tableaux y a la resolución (con sus estrategias de refinamiento).
(Prácticos) Análisis de la complejidad computacional de las tareas
inferenciales. Con esta complejidad en mente, se pretende facilitar
las claves básicas para la implementación de inferencias y el uso
de herramientas disponibles. Y finalmente la representación de problemas
usuales y su resolución sobre este formalismo.
Orientaciones:
Dentro de las actividades de aprendizaje se especifican las lecturas
más adecuadas para cada uno de los objetivos del tema.
Tema 2: Lógicas de Primer Orden
Objetivos:
(Teóricos) Revisión, de nuevo, de conceptos semánticos básicos (modelos,
satisfacibilidad, equivalencia, consecuencia, ...). Estudio en profundidad
de sistemas inferenciales, especialmente tableaux y resolución. Análisis
de la utilidad de esta lógica para las tareas de Representación del
Conocimiento.
(Prácticos) Implementación y herramientas (probadores de teoremas,
entornos lógicos). Referencia a la Programación Lógica y a los problemas
de satisfacción de restricciones.
Orientaciones:
Dentro de las actividades de aprendizaje se especifican las lecturas
más adecuadas para cada uno de los objetivos del tema.
Tema 3: Lógicas Modales
Objetivos:
Apreciar la consecuencias de la evaluación semántica local en la lógica
modal y cómo se corresponde o traduce ésta en fragmentos de la Lógica
de Primer Orden. Revisar las diversas lecturas y usos de las lógicas
modales: lógica proposicional dinámica, lógica epistémica, etc. Consolidar
el análisis semántico común que subyace a todas estas lógicas, sobre
estructuras de Kripke.
Se presentan asimismo tableaux tanto para la lógica modal proposicional
como para su extensión a primer orden. Y se facilitan referencias
a herramientas y probadores en lógicas modales.
Orientaciones:
Dentro de las actividades de aprendizaje se especifican las lecturas
más adecuadas para cada uno de los objetivos del tema.
Tema 4: Lógicas Temporales
Objetivos:
Se presentan inicialmente las lógicas temporales modales (LTL, CTL,
CTL*) para la verificación de sistemas, así como las lógicas modales
espacio-temporales (y su posible aplicación en visión y robótica).
Y se continúa con una revisión de otras lógicas temporales utilizadas
usualmente en Inteligencia Artificial.
Orientaciones:
Dentro de las actividades de aprendizaje se especifican las lecturas
más adecuadas para cada uno de los objetivos del tema.
Tema 5: Lógicas Descriptivas
Objetivos:
Se facilita inicialmente un estudio de las lógicas descriptivas básicas,
con especial atención a su complejidad computacional. Y se continúa
con el estudio de una familia creciente de lógicas descriptivas que
se van obteniendo mediante elección de nuevos descriptores. De todas
ellas se analizará el compromiso entre el aumento de la expresividad
y la complejidad temporal.
Como aplicación de estas lógicas, se sugerirá el estudio de campos
afines como el diseño de ontologías, el manejo de lenguajes como OWL
(para definición de ontologías) y el papel de razonadores descriptivos
(como Racer) en la comprobación de consistencia y en el uso productivo
de tales ontologías.
Orientaciones:
Dentro de las actividades de aprendizaje se especifican las lecturas
más adecuadas para cada uno de los objetivos del tema.
Tema 6: Revisión, limitaciones y alternativas
Objetivos:
En este punto final, se tratará sobre el papel de las lógicas presentadas
en la Representación de Conocimiento y en la resolución de tareas
en IA. A esta reflexión seguirán algunas referencias a lógicas de
orden superior, lógicas no monótonas, lógicas para el manejo de la
incertidumbre... Algunos de estos marcos formales son objeto de estudio
en otras asignaturas del Máster.
Orientaciones:
Dentro de las actividades de aprendizaje se especifican las lecturas
más adecuadas para cada uno de los objetivos del tema.
3 Actividades y plan de trabajo
3.1 Actividades prácticas programadas
* Lógica proposicional: aplicación en problemas concretos, uso de
verificadores de satisfacibilidad como Zchaff
* Lógica de Primer Orden: actividades de Representación de Conocimiento,
uso de probadores como Otter. Alguna incursión en programación lógica
y en actividades sobre problemas de satisfacción de restricciones.
* Lógicas Modales: interacción entre agentes (aplicaciones de la
lógica epistémica). Uso de probadores en lógica modal.
* Lógicas Temporales: actividades breves sobre verificación de sistemas
(con sugerencias de uso de herramientas). Lógicas espacio-temporales.
* Lógicas Descriptivas: representación de conocimiento sobre lógicas
descriptivas de expresividad creciente. Diseño de algunas ontologías.
Servicios inferenciales facilitados por la Lógicas descriptivas. Uso
de Racer. Introducción a OWL
3.2 Otras actividades prácticas programadas
Se irán generando de forma dinámica en el curso virtual.
3.3 Plan de trabajo
Se pretende simultanear el estudio de la teoría con las implementaciones
prácticas y con el uso de entornos lógicos. Esperamos con ello mantener
el nivel de motivación con el que los alumnos comienzan este curso.
Desde el punto de vista teórico, se hará énfasis en comprobar y consolidar
el conocimiento previo sobre lógica de primer orden (o facilitarlo
en caso contrario). Los desarrollos siguientes, en lógicas modales-temporales
y descriptivas, requieren una buena asimilación de los dos primeros
temas.
4 Evaluación
La evaluación se realizará esencialmente a partir del proyecto final
de asignatura. Sin embargo, también se tendrán en cuenta las actividades
realizadas a lo largo del curso.
Reseña del profesorado
Fernández Vindel, José Luis:
José Luis Fdez. Vindel es Profesor del Dpto. de Inteligencia Artificial
de la UNED. Imparte docencia sobre Lógica y Teoría de la Computación
en Primer y Segundo Ciclo de los estudios de Ingeniería Informática,
así como en los estudios de Tercer Ciclo del Dpto.
Su interés actual se centra sobre las Lógicas modales espacio-temporales
y su aplicación en Visión y Robótica; así como en las Lógicas descriptivas
y su papel en el desarrollo de la Web Semántica.
e.mail: jlvindel@dia.uned.es
Heguiabehere, Juan
Juan Heguiabehere cursó sus estudios de Tercer Ciclo en la Universidad
de Amsterdam, donde se doctoró en el ILLC (Institute for Logic, Language
and Computation) en el año 2003. Trabajó posteriormente como Investigador
Asociado en el KRBD Research Center de la Universidad Libre de Bolzano
(Italia). Y actualmente es profesor de la Universidad de Buenos Aires,
su patria natal.
Su interés básico se centra en el desarrollo efectivo de sistemas
inferenciales: modales, en variantes diversas, y descriptivos.
| |
|
|
