Herramientas Matemáticas para la Computación

Sesión Especial nº 12 de MAT.ES 2005

Breve descripción:
La llegada de los ordenadores ha traído consigo una gran cantidad de aplicaciones interesantes para el mundo real y, además, como ha ocurrido con muchos otros avances técnicos, ha propiciado la creación de nuevos campos de investigación tanto a nivel teórico como a nivel práctico.

El vertiginoso ritmo de avance de las Ciencias de la Computación durante la última década del siglo pasado viene provocando la generalización del uso de métodos heurísticos ad hoc para la resolución de problemas. Como consecuencia, se observa una falta de metodología formal unificadora o integradora que proporcione teorías generales que sustenten los métodos desarrollados. La introducción de tales teorías generales proporciona una mayor comprensión de los problemas estudiados y, como consecuencia, frecuentemente provoca inesperados avances al observar los fenómenos con un mayor grado de generalidad.

Objetivos: En esta sesión se pretende dar una visión de distintos temas de investigación matemática con aplicación en computación. El programa constará de varias conferencias invitadas así como charlas cortas de 20 minutos.

Programa

• 31 de enero
  • 9:00-10:00 Acto de Apertura Mat.Es 2005
    
    
  • 10:00-11:00 Conferencia Plenaria Mat.Es 2005
    
    
  • 11:00-13:00 Café
    
    
  • 11:30-12:20 Inma P. de Guzmán: Álgebra y Lógica en Computación (transpas)
    
    Resulta llamativo que la matemática necesaria para la fundamentación formal de la Computación proceda de campos de la matemática tradicionalmente ligados a la Matemática Pura. El objetivo de la charla consiste en presentar una selección de distintas herramientas lógicas y algebraicas para la Computación, mostrando así cómo áreas tales como la Lógica o el Álgebra están teniendo un papel relevante también dentro de la Matemática Aplicada.
    
    
  • 12:20-13:10 Felip Manyà: Resolución de problemas NP-completos utilizando logica proposicional (transpas)
    
    La utilización de las fórmulas booleanas proposicionales como un lenguaje de programación con restricciones para solucionar problemas NP-completos es un área de investigación activa en Inteligencia Artificial. Este nuevo enfoque de resolver problemas combinatorios ha demostrado ser muy competitivo en campos tan diversos como verificación de circuitos, cuadrados latinos, planificación y scheduling. En esta charla presentaremos cómo modelizar problemas NP-completos utilizando fórmulas booleanas proposicionales, y explicaremos las principales estrategias de resolución que incorporan los algoritmos que se utilizan para encontrar modelos de fórmulas booleanas proposicionales.
    
    
  • 13:10-13:30 P. Cordero: MAT Logic: Multi-flow Asynchronic Temporal Logic (transpas)
    
    A new logic-algebraic framework to deal with interactive systems in communication technologies will be presented. This new framework is strongly based on the concept of non deterministic operator. Concretely, the Multi-flow Asynchronic Temporal Logic (called MAT Logic) is presented. MAT Logic is a new temporal x modal logic with non deterministic operators between flows of linear and discrete time. The main goal is the design and description of a logic that could be capable of managing communications between systems with not necessarily synchronizable flows of time. The temporal evolution in every system can be reflected by changes in the states of the system and possible communications between time flows in two systems are given by a lower bounded non deterministic operator. Moreover, effective communications determine a function that change previous lower bounds. The semantic of MAT logic will be exposed in an algebraic style and a minimal axiomatic system dealing with non deterministic operators will be showed.
    
    
  • 13:30-15:30 Almuerzo
    
    
  • 15:30-17:30 Conferencias Plenarias Mat.Es 2005
    
    
  • 17:30-18:00 Café
    
    
  • 18:00-18:50 J. A. Alonso: Desarrollo de teorías computacionales (transpas)
    
    Por teorías computacionales entendemos las teorías desarrolladas en sistemas de razonamiento automático (como ACL2) que permiten tanto la construcción de programas como la demostración automática de propiedades de dichos programas. En este charla presentamos algunas de las teorías computacionales que hemos desarrollado sobre cálculos proposicionales, lógica ecuacional y bases de Gröbner.
    
    
  • 18:50-19:10 J. Martínez: Algebraic axiomatization of multilattice and multisemilattice structures (transpas)
    
    The multisemilattice and multilatice structures, which are the generalization of semilattice and lattice respectively, are very useful for the design of ATP's for temporal and modal logics. For this reason, to have an adequate algebraic characterization for these structures is fundamental. For the multisemilattice structure there is not any algebraic charecterization in the literature, and for the multilattice structure ones, are rather inefficient. We are going to introduce new algebraic characterizations for both structures which are obtained by natural extension of the lattice and semilattice structure.
    
    
  • 19:10-19:30 A. Mora: SL_FD-logic to obtain atomic-minimality in Functional Dependencies (transpas)
    
    We establish an algebraic frame inside lattice theory that has allowed us to establish the concept of redundancy elimination for sets of functional dependencies (FDs) in database and artificial intelligence. All the current FD logics have a common characteristic: The design of their axiomatic system has been guided by the search of the all FDs that are satisfied in a database scheme. On the contrary, we present a novel logic named SL_FD-logic, that has been designed to eliminate redundancy. The problem of removing redundancy in FD sets is presented exhaustively in the bibliography and the authors consider {\em minimality} and optimality criterions for FDs. We relate these criterions and we consider a novel complexity criterion which allows us to introduce a new minimality property for FD sets named atomic-minimality. We use SL_FD-logic rules as a tool to search for atomic-minimality. Also we remark that SL_FD-logic, allow the development of future automated manipulation techniques of functional dependencies directly based on the new axiomatic system.
    
    
  
  
  
• 1 de febrero
  
  
  • 9:00-11:00 Conferencias Plenarias Mat.Es 2005
    
    
  • 11:00-11:30 Café
    
    
  • 11:30-12:20 Patrik Eklund: On Kleene monads (transpas)
    
    Monads are used for various applications in computer science, and wellknown is e.g. the interpretation of morphisms in the Kleisli category of the term monad as variable substitutions assigning terms to variables. An application building upon this observation is the equivalence between most general unifiers and co-equalizers in this category. We show how to use monads with additional structure, namely partially ordered monads, in order to obtain a generalised notion of Kleene powerset algebras building upon more general powerset functor settings beyond strings and relations.
    
    
  • 12:20-13:10 Juan Tena / Daniel Sadornil: Exponenciación modular en anillos de enteros ciclotómicos (transpas)
    
    La exponenciación modular a^m mod n, (con a, m, n naturales) es un problema clásico y el algoritmo de cuadrados repetidos permite su computación eficiente. Sin embargo en ciertos contextos, por ejemplo en relación con generalizaciones del test de primalidad de Proth, el entero a se sustituye por un elemento del anillo de enteros de un cierto cuerpo ciclotómico Q(r), r raíz primitiva de orden r de la unidad. La computación de esta exponenciación generalizada debe pues realizarse en tal anillo Z[r], lo que exige el conocimiento de la estructura y aritmética del mismo.
    Exponemos dos estrategias para la resolución de este problema: la primera expresa el elemento en términos de una base de Z[r]/Z y utiliza las reglas de multiplicación en Z[r]. La segunda utiliza los resultados de la factorización modular del polinomio ciclotómico r.
    Finalmente se muestra una implementacion en Maple para el caso particular r = 5.
    
    
  • 13:10-13:30 A. Valverde: Categorías y unificación generalizada
    
    
  • 13:30-15:30 Almuerzo
  • 15:30-16:20 J.M. Barja / G. Pérez: Formalización de las Bases de Gröbner en Coq (transpas)
    
    Introducimos el concepto de Bases de Gröbner; estudiamos y probamos su equivalencia con otras caracterizaciones alternativas que serán útiles para la construcción de dichas bases. En particular, la que utiliza el Algoritmo de Buchberger para resolver el problema de las "situaciones críticas". Para resolver estas equivalencias damos una versión del Lema de Newman adaptada a nuestra formalización, así como la definición y propiedades de la confluencia y confluencia local de la reducción de polinomios.
    
    
  • 16:20-17:10 Rabindra N. Banerjee: A Geometric approach to resolution: Bridging the Symbolic vs. Connectionist paradigms' gap (transpas)
    
    
  • 17:10-17:30 M. Ojeda: Puntos fijos en programación lógica: no determinismo y dominios potencia. (transpas)
  • 17:30-18:00 Café
    
    
  • 18:00-18:50 J.L. Montaña: Fundamentos Matemáticos del Aprendizaje (transpas)