G.I. de Matemática Aplicada en Computación
Grupo PAIDI TIC 115
Miembros
- Gabriel Aguilera Venegas
- Iván Atencia McKillop
- Pablo Cordero Ortega
- Inmaculada Fortes Ruiz
- Gloria Gutiérrez Barranco
- Nicolás Madríd Labrador
- Javier Martínez del Castillo
- Angel Mora Bonilla
- Emilio Muñoz Velasco
- Manuel Ojeda Aciego
- Inmaculada Pérez de Guzmán Molina
- Estrella Rodríguez Lorenzo
- Francisco Rodríguez Sánchez
- Sixto Sánchez Merino
- Agustín Valverde Ramos
Colaboradores
- Alfredo Burrieza Muñiz
- Manuel Enciso García-Oliveros
- Jesús Medina Moreno
- Carlos Rossi Jiménez
Líneas de trabajo
- Deducción automática.
- Lógicas no estándar: fundamentos y aplicaciones.
- Teoría de categorías y álgebras abstractas para la Computación.
- Teoría de retículos y generalizaciones para la Computación.
- Métodos formales en bases de datos.
Tesis doctorales
- Carlos Guerrero García. Un modelo multicriterio de localización de centros no deseados con pesos. PhD thesis, Universidad de Málaga, España, 2005.
- Salvador Merino Córdoba. Automatización del diseño de torres. PhD thesis, Universidad de Málaga, España, 2003.
- Francisco J. Rodríguez Sánchez. Conexiones de Galois Débiles y nd-operadores de cierre, Razonamiento con Ejemplos. PhD thesis, Universidad de Málaga, España, 2002.
- Angel Mora Bonilla. Dependencias Funcionales, ideal-operadores no deterministas y operadores de sustitución. PhD thesis, Universidad de Málaga, España, 2002.
- Jes™s Medina Moreno. Retículos multiadjuntos y teoremas de continuidad para el operador de consecuencias. PhD thesis, Universidad de Málaga, España, 2002.
- Inmaculada Fortes Ruiz. Prospección de datos, aprendizaje computacional y técnicas estadísticas para la obtención de reglas. PhD thesis, Universidad de Málaga, España, 2002.
- Sixto Sánchez Merino. Sistemas de colas con demandas repetidas y con varios flujos de entrada. PhD thesis, Universidad de Málaga, España, 2002.
- Gloria Gutiérrez-Barranco. Bases de ideales en multirretículos y Delta-¡rboles. PhD thesis, Universidad de Málaga, España, 2001.
- Javier Martínez del Castillo. Omega-álgebras con operadores no deterministas. PhD thesis, Universidad de Málaga, España, 2000.
- P. Cordero. Ideales y filtros de implicados/implicantes en lógicas temporales con tiempo lineal y discreto. PhD thesis, Universidad de Málaga, España, 1999.
- A. Valverde. Δ-árboles de implicantes e implicados y reducciones de lógicas signadas en ATPs. PhD thesis, Universidad de Málaga, España, 1998.
- G. Aguilera. Reducciones totales y parciales para el análisis de validez y construcción de modelos en M3. PhD thesis, Universidad de Málaga, España, 1997.
- M. Ojeda-Aciego. Métodos formales para normalización en lógica de primer orden usando la metodologí a TAS. PhD thesis, Universidad de Málaga, España, 1996.
- M. Enciso. Lógica temporal y demostración automática de teoremas. Eficiencia y paralelismo. PhD thesis, Universidad de Málaga, España, 1995.
- Francisco Sanz. Hacia una alternativa a resolución. PhD thesis, Universidad de Málaga, España, 1992.
Proyectos de Investigación en Curso
TIN2006-15455-C03-01: Lógicas, Deducción y Programación para Sistemas Inteligentes.
El presente proyecto está relacionado con el estudio de los fundamentos matemáticos y posterior desarrollo de la deducción y la programación en varios tipos de lógicas no clásicas, especialmente en lógicas multivaluadas y lógicas intermedias, con vistas a la gestión inteligente de información.
La problemática clásica de la deducción consiste en, dado un conocimiento explícito expresado en un cierto formalismo y un conjunto de reglas de inferencia, deducir conocimiento implícito relevante para las aplicaciones. Más exactamente, estamos interesados en aquellas bases de conocimiento en las que se maneja información incierta o incompleta y en realizar un análisis de información admitiendo preguntas de carácter vago o impreciso.
En este proyecto nos planteamos desarrollar un marco teórico que generalice los distintos enfoques de la programación lógica en contextos difusos mediante el uso de estructuras reticulares generalizadas como conjunto de valores de verdad: birretículos, trirretículos, multirretículos, retículos birresiduados, etc. Para obtener resultados óptimos de cara a la aplicabilidad de estos paradigmas será necesario, además, abordar los dos problemas siguientes: la unificación en estos nuevos contextos, para lo que utilizaremos técnicas categóricas, y la deducción automática en estos sistemas, para lo cual, dado su carácter no canónico, optaremos por la metodología TAS.
Desde el punto de vista de la programación, se buscan extensiones de la programación con conjuntos respuesta (Answer Set Programming, ASP) que a su vez es una generalización de la programación lógica clásica. Estas extensiones de ASP pueden ser implementadas bien sobre implementaciones de ASP, bien mediante sistemas basados en fórmulas booleanas cuantificadas (p.e. QUIP), o bien utilizando la metodología TAS. La importancia de la investigación básica sobre estos sistemas lógicos para la Tecnología del Conocimiento radica en las numerosas aplicaciones potenciales que tales sistemas ofrecen para la modelación y resolución de problemas en áreas como gestión de la información, robótica cognitiva, web semántica, etc.
P06-FQM-02049: Fundamentos Matemáticos de las Lógicas para Sistemas Inteligentes.
TIC2003-09001-C02-01: Deducción y Programación en Lógicas No Clásicas para la Tecnología del Conocimiento.
Investigador principal: Manuel Ojeda Aciego
Este presente proyecto está relacionado con el estudio de los fundamentos matemáticos y posterior desarrollo de la deducción y la programación en varios tipos de lógicas no clásicas, especialmente en lógicas multivaluadas y lógicas intermedias, con vistas a la gestión inteligente de información. La problemática clásica de la deducción consiste en, dado un conocimiento explícito expresado en un cierto formalismo y un conjunto de reglas de inferencia, deducir conocimiento implícito relevante para las aplicaciones. Más exactamente, estamos interesados en aquellas bases de conocimiento en las que se maneja información incierta o incompleta y en realizar un análisis de información admitiendo preguntas de carácter vago o impreciso.
Un primer marco formal elegido es el de la lógica difusa y los distintos paradigmas de programación lógica difusa. Específicamente, en el proyecto nos planteamos desarrollar un marco teórico que generalice los distintos enfoques de la programación lógica en contextos difusos mediante el uso de estructuras reticulares generalizadas como conjunto de valores de verdad: birretículos, trirretículos, multirretículos, retículos birresiduados, etc. Para obtener resultados óptimos de cara a la aplicabilidad de estos paradigmas será necesario, además, abordar los dos problemas siguientes: la unificación en estos nuevos contextos, para lo que utilizaremos técnicas categóricas, y la deducción automática en estos sistemas, para lo cual, dado su carácter no canónico, optaremos por la metodología TAS.
Desde el punto de vista de la programación, se buscan extensiones de la programación con conjuntos respuesta (Answer Set Programming, ASP) que a su vez es una generalización de la programación lógica clásica. Estas extensiones de ASP pueden ser implementadas bien sobre implementaciones de ASP, bien mediante sistemas basados en fórmulas booleanas cuantificadas (p.e. QUIP), o bien utilizando la metodología TAS. La importancia de la investigación básica sobre estos sistemas lógicos para la Tecnología del Conocimiento radica en las numerosas aplicaciones potenciales que tales sistemas ofrecen para la modelación y resolución de problemas en áreas como gestión de la información, robótica cognitiva, web semántica, etc.
TIC2003-08687-C02-01: Las dependencias como eje transversal del tratamiento de los datos: fundamentos algebraicos, sistemas de deducción y herramientas eficientes.
Investigador principal: Inmaculada Pérez de Guzmán Molina
En bases de datos está tomando mucha relevancia el estudio de las relaciones entre los datos, sea en su vertiente de dependencias (de diversos tipos) o de asociaciones. Estas interrelaciones entre datos pueden concebirse como reglas de integridad que proporcionan información sobre la estructura de la base de datos y que, por tanto, pueden ayudar a su diseño y también a su manipulación. En esta propuesta se pretende dar una solución a la especificación y manipulación uniforme de esta información.
Habitualmente estas reglas de integridad son tratadas de forma independiente (por un lado las dependencias funcionales, por otro las dependencias difusas, etc) y en general las investigaciones se centran en cómo descubrir nuevas relaciones a partir de la propia base de datos (usando por ejemplo técnicas de minería de datos). En lugar de ello es posible acudir a un tratamiento uniforme de diversos tipos de estas reglas o dependencias y desarrollar métodos deductivos para descubrir otras nuevas a partir de la existentes. Ambas aproximaciones sólo no son incompatible, sino que se complementan, pues las reglas deducidas permiten podar los métodos de búsqueda sobre la base de datos y reglas descubiertas en la minería de datos aporta nuevos elementos para deducir nueva información.
En esta propuesta usaremos la lógica como herramienta de representación de diversos tipos de relaciones entre datos (concretamente, abordaremos de modo uniforme las dependencia funcionales, dependencias multivaluadas, dependencias de inclusión, dependencias difusas y dependencias temporales) y realizaremos el desarrollo de sistemas deductivos eficientes para estas reglas de la base de datos.
Para el desarrollo de esta propuesta contamos con la experiencia del subgrupo de la Universidad de Granada en el estudio de la información imprecisa, en el desarrollo de unos operadores relacionales difusos para bases de datos y la imlementación de herramientas para el desarrollo de una base de datos difusa, así como con la experiencia del sugrupo de Málaga en el diseño de muy diversos tipos de lógicas computacionales (modales, temporales, de dependencias funcionales, etc) y en la creación e implementación de sistemas de deducción para dichas lógicas, donde la eficiencia proviene de la aplicación perezosa de las tareas que se encargan de las etapas de coste exponencial de cada proceso de deducción.
HP2001-0078: Programación Lógica Residuada.
TIC2000-1109: Sistema de información para la gestión inteligente de archivos y documentos. Optimización de la manipulación de la información con software deductivo.
Investigador principal: Inmaculada Pérez de Guzmán Molina
A medida que las tecnologías de la información se están imponiendo en los sectores productivos, la digitalización de los archivos se revela como una necesidad que las empresas dedicadas a estos sectores deben afrontar y a la que es necesario aportar soluciones. La digitalización no sólo tiene aspectos positivos para la empresa que la aplica, sino que sus beneficios trascienden a la misma en tanto que elimina una gran cantidad de papel, lo cual redunda en un beneficio sobre el medio ambiente. De hecho, el mercado ha ido evolucionando y el cliente final comienza a demandar este producto de forma continuada.
Las aplicaciones comerciales de almacenamiento de archivos y documentos tienen la característica común de que el almacenamiento de la información no se realiza en una base de datos abierta (Oracle, Informix, etc), sino que disponen de un sistema de archivos propio. Esta característica presenta las siguientes desventajas:
- Las empresas que adquieren estos productos están ligadas a esta aplicación y no les es posible realizar aplicaciones compatibles con la base de datos ajustadas a sus necesidades.
- El sistema de archivos resulta ser menos potente que una base de datos comercial en aspectos tan importantes como la seguridad de la información, la optimización de consultas, las características físicas de¡ almacenamiento, etc.
- La adaptación de estos productos a las nuevas tecnologías de bases de datos es muy limitada. Es común que las soluciones que incorporan los gestores de bases de datos no pasen a estos productos hasta que los clientes lo demandan insistentemente, cosa que, en general, sucede con dos o tres años de desfase.
En este documento proponemos el desarrollo de una tecnología propia que permita disminuir los costes de¡ almacenamiento de documentos una vez digitalizados. De esta forma se dispondrá de un sistema dotado de las innovaciones tecnológicas introducidas en los últimos años, en cuanto a las herramientas empresariales y las comunicaciones.
El sistema propuesto se basará en una arquitectura de base de datos por capas; concretamente, se desarrollará de una capa de acceso a la información almacenada en una base de datos comercial que disponga de la potencia que ésta aporta y cuente además con las siguientes características suplementarias:
- Enriquecimiento del lenguaje de manipulación de base de datos con características temporales. Las bases de datos de documentos disponen de un conjunto de restricciones temporales que debe ser mantenido. Además, en gran cantidad de ocasiones, constituyen una base de datos histórica y para su eficiente manipulación natural se precisa de una mayor potencia expresiva.
- Uso de la Lógica Temporal como sustrato subyacente al lenguaje de manipulación de bases de datos. Esta característica es demandada para dotar al sistema de una base formal que permita la mejora de la eficiencia como se describe en el punto siguiente.
- Aumento de la potencia M optimizador de consultas mediante el uso de transformaciones de las expresiones de la Lógica Temporal utilizando métodos de demostración automática.
- La existencia de un lenguaje temporal de acceso a bases de datos lleva consigo una mayor aparición de valores nulos, pues ahora dichos valores no representan sólo desconocimiento de la información, sino también su ausencia o carencia de sentido en un cierto periodo de tiempo. Para anular este efecto, incluimos el uso de Lógica Multivaluada y de las transformaciones correspondientes derivadas de la demostración automática de teoremas.
Estas características dictan claramente los dos módulos de la arquitectura de base de datos que deben ser modificados, el intérprete de los lenguajes de definición y manipulación de base de datos y el optimizador de consultas. Construiremos una capa superior al propio gestor e independiente de éste, que nos permita dotar de estas novedosas características a cualquier aplicación de almacenamiento de archivos digitalizados construida sobre cualquier gestor de base de datos relaciona¡.
BFM2000-1054-C02-02: Deducción Automática No Canónica.
El presente proyecto se integra dentro del campo de la Deducción Automática. La problemática clásica de este campo consiste en, dado un conocimiento explícito expresado en un cierto formalismo y un conjunto de reglas de inferencia, deducir conocimiento implícito relevante para las aplicaciones.
Actualmente, el problema se concreta, en el ámbito de diversas áreas temáticas tanto de la Ingeniería como de las Ciencias de la Computación, como la necesidad de un software deductivo que es reclamado por una amplia gama de aplicaciones tales como bases de datos deductivas, sistemas de seguridad crítica, sistemas en tiempo real, robótica, sistemas multiagestes, control de procesos, etc.
Dada la gran variedad de tipos de conocimiento requeridos en las diversas áreas cognitivas, diferentes formalismos de representación están siendo considerados por la comunidad investigadora. Siguiendo esta línea, en este proyecto exploraremos diversos métodos de representación complementarios entre sí y abarcando tanto lenguajes clásicos como de reciente actualidad. También analizaremos la manera en que cada lenguaje considerado peculiariza las relglas de inferencia y el modo en que éstas deben encadenarse con eficiencia en un proceso deductivo.
Los lenguajes que serán estudiados se circunscriben a la deducción lógica no canónica. Más concretamente, profundizaremos en los sistemas deductivos basados en
- Formas no clausales
- Teorías con relaciones binarisa especiales
- Unificación en contextos no canónicos
- Sintaxis diagramáticas
Por lo tanto, nuestro propósito es estudiar y desarrollar diversos sistemas deductivos con diferentes formalismos de representación lógica no canónica.
TIC97-0579-C02-02:Modelización y Síntesis en Diseños Lógicos de Sistemas Informáticos: de la Formalización a las Aplicaciones.
Dentro de la Lógica Computacaional, de los Métodos Formales y la Inteligencia Artificial en general, existen numerosas técnicas con enorme potencial para la modelización de procesos industriales y comerciales. Sin embargo, debido a la insuficiente antención prestada a los aspectos pragmñáticos de dichas técnicas, todavía existe una gran distancia entre la conceptualización de un problema y la obtención de su primer modelo o prototipo ejecutable.
Nuestro proyecto quiere contribuir a paliar dicho problema. Nuestro objetivo general es desarrollar una metodología e implementar un sistema de especificación formal donde se incorporen algunas de dichas técnicas haciéndolas accesibles a usuarios no informáticos mediante la adaptación de aquellas a las prácticas de éstos y no viceversa.
El objetivo es permitir la construcción y evaluación rápida de prototipos preliminares de los modelos industriales y comerciales, disminuyendo la presión y dificultad actual por obtener la primera versión del modelo. El sistema propuesto se basa, por una parte, en la idea de especificación por colaboración. Cada participante en la especificación contribuye a ella a un nivel adecuado a su propia experiencia con las notaciones y herramientas que le son familiares, existiendo entre los distintos nivele notaciones y herramientas de descripción puntos de contacto e interfaces claras. Por otra parte, siendo la lógica computacional el punto de anclaje de todas esta técnicas nuestro mecanismo deductivo debe permitir un diseño modular capaz de razonar en contextos temporales específicos, con información incompleta y que posibilite la actualización en tiempo real de las bases de conocimiento; aspectos irrenunciables si se pretende aplicarlos a problemas concretos.
Estos dos aspectos en los que los proponentes poseen ya experiencia tienen interés en sí mismos y son confluyentes en las aplicaciones. La elaboración de esta propuesta ha sido diseñada para asegurar su viabilidad tanto en los aspectos teóricos como en los prácticos, acordes éstos con la fisonomía del Parque Tecnológico de Andalucía en Málaga.
TIC94-0847-C02-02:Descripción Incremental de Sistemas basada en el Cálculo de Refinamientos y Lógicas Modales Ejecutables. Aplicaciones a los Sistemas de Seguridad Crítica.
La investigación conducente al desarrollo de software seguro y fiable que pueda ser utilizado en aplicaciones tales como Bases de Datos Temporales activas, Sistemas de Seguridad Crítica y Sistemas Multiagentes, tiene gran interés científico e industrial. Existen sistemas comerciales de gestión de especificaciones y programas, pero carecen de una rigurosa base formal y por tanto están limitados en cuanto a generalidad y fiabilidad.
Por otra parte, los sistemas formales para la especificación de requerimientos que existen, sólo se han aplicado a pequeños problemas o a limitados aspectos de la captura de requerimientos. En este proyecto se apuesta, en primer lugar, por la aplicación de las técnicas de la lógica computacional a la especificación de requerimientos de problemas reales como son los mencionados, especialmente los Sistemas de Seguridad Crítica.
En el subproyecto 1, entendemos esta tarea como un proceso de refinamiento entre varios niveles de detalle de la especificación del sistema. En cada etapa es posible comprobar propiedades y la coherencia de una versión respecto a la anterior en el proceso de refinamiento. Una vez completa la especificación se podrán aplicar métodos de transformación hacia programas más eficientes. Esta metodología está fundada en un lenguaje de especificación básico (COR), rigurosamente fundamentado y fácil de entender, apto para su extensión incremental según las necesidades del usuario.
En el subproyecto 2, entendemos que, en el área de los Sistemas de Seguridad Crítica, los lenguajes neutrales respecto al fenómeno en el dominio del problema, no se adecúan a la axiomatización del conocimiento. Por lo tanto, son necesarios lenguajes de programación que permitan la representación de este conocimiento sobre el dominio y, debido a que las aplicaciones consideradas tienen en común la necesidad de razonar sobre conocimiento, tiempo y creencia, es bastante aceptado que los lenguajes requeridos han de ser lenguajes basados en lógicas modales y temporales. Con esta visión, adoptamos como punto de partida para la búsqueda de mecanimos de ejecución, formas ejecutables de lenguajes modales y temporales (LMex), siguiendo técnicas bien contrastadas.
