Descripción del proyecto
LOS PROBLEMAS DIFICILES DE SATISFACCION Y OPTIMIZACION ESTAN PRESENTES EN MUCHAS APLICACIONES COMPUTACIONALES, ALGUNOS DESAFIOS SON: HACER LOS HORARIOS DE UNA LIGA DE DEPORTE PROFESIONAL, DETERMINAR SI UN PROTOCOLO CRIPTOGRAFICO ES SEGURO, SABER SI UNA COMBINACION DE DATOS DE ENTRADA PUEDE ORIGINAR QUE UN PROGRAMA "SE CUELGUE" O DE UN RESULTADO ERRONEO, DETERMINAR EL TIEMPO MAS ADECUADO PARA UNA VIDEO CONFERENCIA, DEFINIR UN CONTROL DE ADMISION FLEXIBLE PARA UN "OVERBOOKING" SEGURO EN COMPUTACION EN NUBE, O CATALOGAR Y RECUPERAR UN TEXTO DE FORMA FLEXIBLE EN LA WEB SEMATICA,UNA APROXIMACION DECLARATIVA PARA RESOLVER DICHOS PROBLEMAS CONSISTE EN MODELIZAR EL PROBLEMA EN CUESTION EN ALGUN FORMALISMO LOGICO, Y ENTONCES APLICAR TECNICAS POTENTES BASADAS EN LOGICA PARA ANALIZAR Y RESOLVER EL MODELO RESULTANTE, EN ESTA LINEA, LOS PROBLEMAS A MENUDO SE PUEDEN FORMULAR USANDO FORMULAS MATEMATICAS O OTROS LENGUAJES BASADOS EN LOGICA, UNA VEZ QUE EL PROBLEMA ESTA EXPRESADO EN EL LENGUAJE CORRESPONDIENTE, PODEMOS UTILIZAR TECNICAS GENERALES EXISTENTES O DESARROLLAR NUEVAS TECNICAS PARA RESOLVERLO, CUANDO ESTA APROXIMACION SE APLICA A PROBLEMAS ESPECIFICOS, PODRIAMOS UTILIZAR ALGUNAS DE SUS PARTICULARIDADES PARA MEJORAR SU RENDIMIENTO, SIN EMBARGO, GRACIAS A LA ABSTRACCION INICIAL DE PROBLEMAS PARTICULARES A PROBLEMAS GENERALES EXPRESADOS EN UN LENGUAJE DADO, ESTA "APROXIMACION DECLARATIVA" HACE QUE EL DESARROLLO DE HERRAMIENTAS PARA RESOLVER PROBLEMAS REALES DIFICILES SEA MAS FACIL Y RAPIDO,COMO FORMALISMS LOGICOS, USAREMOS PRINCIPALMENTE (EXTENSIONES DE) LA LOGICA PROPOSICIONAL Y DE PRIMER ORDEN, EN PARTICULAR, CONSIDERAREMOS: SAT (SATISFACCION DE FORMULAS PROPOSICIONALES), SAT MODULO TEORIAS (SMT, DONDE PROPOSICIONES SE SUSTITUYEN POR ATOMOS EN LA TEORIA DADA), PROGRAMACION CON RESTRICCIONES (CP, DONDE LAS CLAUSULAS SE SUSTITUYEN POR PREDICADOS SOBRE UN LENGUAJE PREDEFINIDO), LOGICA DIFUSA (FL, DONDE LAS CLAUSULAS TIENEN INCERTIDUMBRE), LOGICA DE REESCRITURA (RWL, CON CAPACIDADES AVANZADAS PARA MODELIZAR Y PROGRAMAR), PROGRAMACION LOGICA (LP), Y PROGRAMACION LOGICA DIFUSA (FLP), EN ESTE PROYECTO NOS ENFOCAREMOS SOBRE LA COMBINACION Y EXTENSION DE ESOS LENGUAJES FORMALES EXITOSOS PARA OBTENER LA EXPRESIVIDAD NECESARIA PARA NUESTRAS APLICACIONES PRACTICAS,GUIADOS POR APLICACIONES PARA PROGRAMACION DE TAREAS Y PLANIFICACION, PARA SEGURIDAD, PARA AGENTES, PARA APRENDIZAJE AUTOMATICO, PARA ANALISIS DE PROGRAMAS SECUENCIALES Y CONCURRENTES, PARA BIOINFORMATICA O PARA MANIPULACION DE XML, DESARROLLAREMOS ALGORITMOS Y HERRAMIENTAS EFICIENTES PARA RESOLVER PROBLEMAS DESCRITOS EN LOS FORMALISMOS LOGICOS MENCIONADOS,COMO APLICACIONES CONCRETAS, CONSIDERAMOS: (A) PROGRAMACION DE DEPORTES,COMO LAS REALIZADAS CON HYPERCUBE Y KNVB EN HOLANDA, (B) ANALISIS DE PROGRAMAS EN COLABORACION CON MICROSOFT RESEARCH EN CAMBRIDGE, (C) EVALUACION DE SECUENCIAS DE TRANSCRIPCION EN COLABORACION CON EL CENTRO DE REGULACION GENOMICA EN BARCELONA, (D) SEGURIDAD EN COLABORACION CON LA UNIVERSIDAD DE ILLINOIS EN URBANA-CHAMPAIGN Y EL NAVAL RESEARCH LABORATORY EN WASHINGTON, (E) NUEVAS CARACTERISTICAS EN EL LENGUAJE MAUDE EN COLABORACION CON LA UNIVERSIDAD DE ILLINOIS EN URBANA-CHAMPAIGN Y SRI INTERNATIONAL EN CALIFORNIA, (F) DESCUBRIR CONOCIMIENTO Y MANIPULACION FLEXIBLE DE DATOS RECUPERADOS DE LA WEB EN COLABORACION CON LA UNIVERSIDAD DE ALMERIA, Y (G) PROGRAMACION DIFUSA PARA RECURSOS DENTRO DE CENTRO DE DATOS DE LA NUBE EN COLABORACION CON UNIV UMEA, LÓGICAS\ RESOLUCIÓN DE RESTRICCIONES\ SATISFACIBILIDAD DE FÓRMULAS\ ANÁLISIS Y VERIFICACIÓN DE PROGRAMAS