El trabajo incluido en la presente tesis se enmarca dentro del campo de la demostración automática de teoremas y consiste en la estudio, definición y desarrollo de un paradigma de resolución lineal, denominado Resolución SL*. La razón para utilizar la denominación de paradigma reside en el hecho de que en sí misma resolución SL* no es un procedimiento, sino que se puede entender como una forma de razonamiento con ciertos parámetros cuya instanciación da lugar a diferentes procedimientos que son adecuados para el tratamiento de distintos tipos de problemas. Por otro lado, se le ha dado el nombre de resolución SL* porque, como posteriormente se explicará, está muy cercano a Eliminación de Modelos y a resolución SL (de ahí la primera parte del nombre). El asterisco final quiere denotar su parametrización, de forma que los procedimientos instancias de resolución SL* serán denominados con una letra más en vez del asterisco, como posteriormente se verá. La tesis ha sido dividida en cuatro capítulos que se describen brevemente a continuación. En el primero se realiza una breve introducción histórica a la demostración automática, que va desde los orígenes de la lógica con el uso de las primeras notaciones matemáticas formales en el siglo XVI hasta la aparición de los resultados más importantes de la lógica descubiertos por Herbrand, Gödel, Church, etc. Se hace un especial hincapié en este capítulo en la demostración automática realizando un recorrido desde sus orígenes a finales del siglo XVIII hasta el momento actual, en el cual es posible ver cuál ha sido la evolución de este campo y qué descubrimientos y resultados se pueden presentar como los principales puntos de inflexión. En el segundo capítulo se presentan la resolución lineal y algunos de sus principales refinamientos, ya que resolución SL* es un variación de resolución SL y por tanto de resolución lineal. Para ello se introduce el principio de resolución, viendo los problemas de su mecanización, y posteriormente se ven dos refinamientos de resolución: resolución semántica y resolución lineal. Para concluir se estudian los principales refinamientos de resolución lineal: resolución de entrada, resolución lineal con fusión, resolución lineal con subsumción, resolución lineal ordenada, resolución MTOSS y TOSS, Eliminación de Modelos, resolución SL y el sistema MESON. En el tercer capítulo se presentan y estudian con profundidad las principales aportaciones al campo de la demostración automática que se han producido en los últimos años y que están cercanas a la aproximación del presente trabajo. Se han incluido los siguientes trabajos: el demostrador PTTP de Stickel, el sistema MESON basado en secuencias de Plaisted, el demostrador SATCHMO de Manthey y Bry, los procedimientos Near-Horn Prolog de Loveland y otros autores y, por último, el demostrador SETHEO de Bibel y otros autores. Obviamente no se han incluido todos los demostradores y procedimientos, pero sí aquellos que se han considerado como los más interesantes y cercanos a resolución SL* de manera que sea posible realizar comparaciones, de forma que queden patentes las aportaciones realizadas. En el cuarto capítulo se presenta resolución SL*. Se da la definición formal de la misma y se introduce el concepto fundamental de elección de ancestros. La elección de ancestros es el mecanismo que permite controlar la aplicación de la resolución de ancestro haciendo posible una reducción del coste de su aplicación y una adecuación de resolución SL* al tipo de problema a tratar. Posteriormente se ven las principales instancias de resolución SL*, los procedimientos SLT y SLP. En este capítulo se hace un especial hincapié en la elección de ancestros, ya que es la principal aportación de resolución SL*, analizando tanto las ventajas que aporta asociadas al incremento de la eficiencia como el hecho de dotar a resolución SL* la capacidad de adaptarse a los problemas que trata. También en este capítulo se presenta una implementación de resolución SL*, en particular del procedimiento SLT, y se incluyen resultados sobre un conjunto extenso de problemas del campo de la demostración automática. En la última sección de este capítulo se realiza una comparación de resolución SL* con los demostradores y sistemas más cercanos, tanto a nivel de características como de resultados. / Casamayor Rodenas, JC. (1996). Resolución SL*: Un paradigma basado en resolución lineal para la demostración automática [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/6023 / Palancia

[ES] La evaluación parcial de programas es una técnica general y potente de optimización de programas que preserva su semántica y tiene muchas aplicaciones relevantes. La optimización se consigue al especializar programas con respecto a una parte de sus datos de entrada, lo que produce un nuevo programa llamado residual o programa especializado tal que, al ejecutarlo con los datos de entrada restantes, producirá el mismo resultado que produce el programa original con todos sus datos de entrada. Los esquemas de evaluación parcial existentes no son aplicables a lenguajes expresivos basados en reglas como Maude, CafeOBJ, OBJ, ASF+SDF y ELAN, los cuales soportan: 1) sofisticados tipos estructurados con subtipos y sobrecarga de operadores; y 2) teorías ecuacionales modulo varias combinaciones de axiomas tales como asociatividad, conmutatividad e identidad. Esta tesis desarrolla las bases teóricas necesarias e ilustra los conceptos principales para su aplicación a programas expresivos escritos en el lenguaje Maude. El esquema de evaluación parcial presentado en esta tesis está basado en un algoritmo automático de desplegado que computa variantes de términos. Para asegurar la terminación del proceso de especialización se han diseñado algoritmos de alto rendimiento para la generalización ecuacional menos general con tipos ordenados y subsunción homeomórfica ecuacional con tipos ordenados. Se muestra que la técnica de evaluación parcial desarrollada es correcta y completa para teorías de reescritura convergentes que pueden contener varias combinaciones de axiomas de asociatividad, conmutatividad y/o identidad para diferentes operadores binarios. Finalmente se presenta Victoria, el primer evaluador parcial para teorías ecuacionales de tipos ordenados para el lenguaje Maude, y se demuestra la efectividad y el incremento en eficiencia ganado a través de experimentos realizados con ejemplos reales. / [CAT] L'avaluació parcial de programes és una tècnica general i potent d'optimització de programes que preserva la seua semàntica i té moltes aplicacions rellevants. L'optimització s'aconseguix a l'especialitzar programes respecte a una part de les seues dades d'entrada, la qual cosa produïx un nou programa cridat residual o programa especialitzat tal que, a l'executar-ho amb les dades d'entrada restants, produirà el mateix resultat que produïx el programa original amb totes les seues dades d'entrada. Els esquemes d'avaluació parcial existents no són aplicables a llenguatges expressius basats en regles com Maude, CafeOBJ, OBJ, ASF+SDF i ELAN, els quals suporten: 1) sofisticats tipus estructurats amb subtipus i sobrecàrrega d'operadors; i 2) teories equacionals mòdul diverses combinacions d'axiomes com asociativitat, conmutativitat i identitat. Esta tesi desenrotlla les bases teòriques necessàries i il·lustra els conceptes principals per a la seua aplicació a programes expressius escrits en el llenguatge Maude. L'esquema d'avaluació parcial presentat en esta tesi està basat en un algoritme automàtic de desplegat que computa variants de termes. Per a assegurar la terminació del procés d'especialització s'han dissenyat algoritmes d'alt rendiment per a la generalització ecuacional menys general amb subtipus ordenats i subsunción ecuacional homeomórfica amb subtipus ordenats. Es mostra que la tècnica d'avaluació parcial desenrotllada és correcta i completa per a teories de reescriptura convergents que poden contindre diverses combinacions d'axiomes d'asociativitat, conmutativitat i identitat per a diferents operadors binaris. Finalment es presenta Victoria, el primer avaluador parcial per a teories equacionals de tipus ordenats per al llenguatge Maude i es demostra l'efectivitat i l'increment en eficiència guanyat a través d'experiments realitzats amb exemples reals. / [EN] Partial evaluation is a powerful and general program optimization technique that preserves program semantics and has many successful applications. Optimization is achieved by specializing programs w.r.t. a part of their input data so that, when the residual or specialized program is executed on the remaining input data, it produces the same outcome than the original program with all of its input data. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: 1) rich type structures with sorts, subsorts, and overloading; and 2) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity. This thesis develops the new foundations needed and illustrates the key concepts of equational order sorted partial evaluation by showing how they apply to the specialization of expressive programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on high-performance order-sorted equational least general generalization and ordersorted equational homeomorphic embedding algorithms for ensuring termination.We show that our partial evaluation technique is sound and complete for order-sorted equational theories that may contain various combinations of associativity, commutativity, and/or identity axioms for different binary operators. Finally, we present Victoria, the first partial evaluator for Maude's order-sorted equational theories, and demonstrate the effectiveness of our partial evaluation scheme on several examples where it shows significant speed-up. / Finally, I extend my thanks to SENESCYT for the support provided for my studies. Also, I thank the Universidad de Guayaquil that is my place of work. / Cuenca Ortega, ÁE. (2019). Partial Evaluation of Rewriting Logic Theories [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/130206 / TESIS

El Análisis de Autoría (AA) es una subtarea en el campo de la Minería de Datos (MD), donde se persigue el propósito de minar un estilo o patrón de redacción correspondiente y característico de un autor, a partir de los documentos redactados por el mismo. Una de las aplicaciones o enfoques más analizados en la comunidad internacional se corresponde con determinar el autor de un documento anónimo o uno cuyo autor esté en duda. Para esto es necesario intentar inferir características del estilo de redacción del autor a través de los documentos escritos por él, estas características nos permitirán conformar un modelo del estilo de este autor y medir qué tan similar puede ser un documento cualquiera a los documentos escritos por dicho autor. Un caso de estudio práctico en las ciencias forenses se manifiesta cuando el perito debe evaluar la autoría de un documento desconocido y solo cuenta con muestras certificadas de un autor, para lo cual debe responder si fue redactado o no por el consiguiente autor, se puede abstener o en qué grado pudo ser redactado, entre otros elementos, atendiendo a la semejanza con las muestras conocidas. Este caso de estudio se corresponde con las investigaciones realizadas en la Verificación de Autoría (VA). Al proceso que trata de determinar la autoría de un documento digital a partir de las muestras digitales conocidas de uno o más autores se conoce como Verificación de Autoría Intrínseca (VAI). La propuesta se centra en el diseño y la implementación de métodos supervisados de VAI orientado a una sola clase, donde solo se empleen muestras conocidas de un autor y se analicen las características contenidas en la redacción de cada documento (enfoque basado en instancias) y otra variante donde a partir de las muestras conocidas de autor se crea un nuevo documento ficticio que contiene información de todos los documentos (enfoque basado en prototipo). Los resultados obtenidos son alentadores y permiten evaluar la utilidad y generalización de nuestra propuesta ante diferentes escenarios y dominios de aplicación. En lo fundamental se manifiesta la importancia de disponer de más de una muestra conocida para cada autor que se desee analizar. Los mejores resultados se obtienen para las colecciones con mayor promedio de palabras por documentos y número de muestras por autores. Se aprecia que la combinación de los resultados en las decisiones permite obtener una mayor efectividad que si solo se empleara una función de comparación y una representación de los documentos empleando un solo tipo de rasgo.

La Biblioteca Virtual Miguel de Cervantes, con dirección web http://www.cervantesvirtual.com, es una biblioteca digital española creada en 1999 con el objetivo principal de difundir la cultura hispánica. Siguiendo los pasos de las grandes bibliotecas, a principios de 2015 la BVMC lanzó su primera versión de datos abiertos basada en el vocabulario RDA que se encuentra disponible en la dirección http://data.cervantesvirtual.com. El proyecto de datos abiertos de la BVMC tiene como objetivos promover la compartición y reutilización de datos, así como la difusión de buenas prácticas. Esta tesis presenta los pasos seguidos para publicar y enriquecer semánticamente los datos abiertos de la BVMC e incluye las siguientes aportaciones: • Construcción de un entorno de publicación y enriquecimiento de datos abiertos que permite comprender mejor el contexto, los problemas y necesidades organizacionales, reduciendo las posibilidades de fracaso de este tipo de proyectos. • Establecimiento de una metodología que sistematiza y facilita el descubrimiento e identificación de entidades en un dominio de bibliotecas digitales. • Desarrollo de herramientas y algoritmos para automatizar el procesamiento de conjuntos de datos basados en registros bibliográficos de manera eficiente. • Propuesta de una metodología para la evaluación de la calidad de los datos que incluye la precisión, la consistencia y la accesibilidad, entre otros criterios. Como resultado del trabajo realizado se han publicado tres artículos en revistas indexadas, dos de ellos en Journal of Information Science y uno en Semantic Web Journal, además una publicación en la conferencia Advances in Information Retrieval, así como numerosas comunicaciones a nivel nacional e internacional, en colaboración con otras instituciones.

En la actualidad, las tecnologías de la información y comunicación (TIC) se han convertido en herramientas invaluables en el desarrollo de la sociedad. Estas tecnologías están presentes en las empresas, la medicina, la educación, etc. Prácticamente la sociedad ha llegado a un punto en que el principal asistente en cada una de las actividades son las TIC. Esto ha permitido la globalización de todas las áreas donde estas son aplicadas. Las ventajas del uso de las TIC han permitido mejorar y automatizar los procesos en todo nivel, sea en una empresa, una ciudad, una universidad, un hogar, etc. Para hacerlo, las tecnologías se ajustan a las necesidades del usuario y son capaces de interactuar con él, incluso, están en capacidad de interactuar entre sí sin la intervención de un humano. ¿Pero cómo lo hacen y para qué? Las nuevas tecnologías ahora integran varios sistemas y plataformas que están en la capacidad de adquirir información de las personas y sus entornos, analizar esta información y tomar decisiones con base en los resultados del análisis. Estas decisiones se ven plasmadas, por ejemplo, en la mejora de las ventas de una empresa o en la mejora de los procesos de manufactura. Como estos, existen muchos ejemplos que son resultado de numerosas investigaciones que tienen como objetivo mejorar la calidad de vida de las personas en ecosistemas sostenibles. Uno de estos ecosistemas que ha adquirido gran importancia recientemente son las ciudades inteligentes. El valor de las ciudades inteligentes se basa en satisfacer las necesidades de los miembros de su comunidad en armonía con la naturaleza. Esto involucra una mejor administración de los servicios como el transporte, la generación y consumo energético, la seguridad, la gobernabilidad, etc. Sin embargo, transformar una ciudad común en una ciudad inteligente requiere de muchos esfuerzos y recursos, tanto económicos como humanos. Ante este problema, es necesario contar con escenarios similares que incluso sirvan como un banco de pruebas para la implementación de tecnologías y que su implementación en entornos más grandes sea efectiva y con los recursos adecuados. Las universidades, como generadoras de conocimiento, son las llamadas a realizar los procesos de implementación, pruebas y generación de nuevas tecnologías. Su ambiente, administración y organigrama estructural, sumada a extensas áreas que conforman sus campus, permite compararlas con pequeñas ciudades. Esto permite establecer una línea base donde se apliquen todos los componentes necesarios para transformarlos en campus inteligentes (smart campus). Los campus inteligentes buscan mejorar la calidad de la educación a través de la convergencia de nuevas tecnologías. Es importante establecer que un campus universitario pone a disposición de los estudiantes y los miembros de la comunidad todas las condiciones para garantizar la calidad de la educación. Los campus inteligentes, al igual que las ciudades inteligentes, basan sus entornos en satisfacer las necesidades de sus miembros; para esto, es necesario crear procesos o sistemas que adquieran información sobre ellos. Es por esto, que el Internet de las cosas (IoT, acrónimo en inglés de Internet of Things) se convierte en uno de los componentes necesarios para la transformación de un campus tradicional. La información recolectada necesariamente debe convertirse en conocimiento para ejecutar acciones con base en este conocimiento. Estas acciones responden a una toma de decisiones efectiva y eficiente que satisfaga las necesidades de las personas. Para realizar el análisis de datos es necesario contar con una arquitectura que gestione un gran volumen de datos independientemente de su formato. La tecnología que ofrece estas capacidades es el big data, su integración al campus inteligente genera una estructura lo suficientemente robusta para soportar toda la carga del IoT y el análisis de datos requerido por los usuarios. Estas tecnologías, en compañía de la computación en la nube (cloud computing), permiten a los miembros del campus inteligente desarrollar sus actividades en total armonía con los recursos y la naturaleza. Este trabajo de investigación está enfocado en proponer una arquitectura para la gestión de datos en un campus universitario. Este enfoque trata todas las variables que influyen en la educación universitaria. Descubrir estas variables, tratarlas y establecer sus relaciones entre sí, requiere de la integración de las tecnologías mencionadas incluso con modelos de inteligencia artificial que permitan tomar acciones sobre los resultados del análisis de datos.

[EN] Nowadays, undetected programming bugs produce a waste of billions of dollars per year to private and public companies and institutions. In spite of this, no significant advances in the debugging area that help developers along the software development process have been achieved yet. In fact, the same debugging techniques that were used 20 years ago are still being used now. Along the time, some alternatives have appeared, but there still is a long way for them to be useful enough to get into the software development process. One of them is algorithmic debugging, which abstracts the information the user has to investigate to debug the program, allowing them to focus on what is happening instead of how it is happening. This abstraction comes at a price: the granularity level of the bugs that can be detected allows for isolating wrongly implemented functions, but which part of them contains the bug cannot be found out yet. This thesis focusses on improving algorithmic debugging in many aspects. Concretely, the main aims of this thesis are to reduce the time the user needs to detect a programming bug as well as to provide the user with more detailed information about where the bug is located. To achieve these goals, some techniques have been developed to start the debugging sessions as soon as possible, to reduce the number of questions the user is going to be asked about, and to augment the granularity level of those bugs that algorithmic debugging can detect, allowing the debugger in this way to keep looking for bugs even inside functions. As a result of this thesis, three completely new techniques have been defined, an already existent technique has been improved, and two new algorithmic debugging search strategies have been defined that improve the already existent ones. Besides these theoretical results, a fully functional algorithmic debugger has been implemented that contains and supports all these techniques and strategies. This debugger is written in Java, and it debugs Java code. The election of this language is justified because it is currently one of the most widely extended and used languages. Also because it contains an interesting combination of unsolved challenges for algorithmic debugging. To further increase its usability, the debugger has been later adapted as an Eclipse plugin, so it could be used by a wider number of users. These two debuggers are publicly available, so any interested person can access them and continue with the research if they wish so. / [ES] Hoy en día, los errores no detectados de programación suponen un gasto de miles de millones al año para las empresas e instituciones públicas y privadas. A pesar de esto, no ha habido ningún avance significativo en el área de la depuración que ayude a los desarrolladores durante la fase de desarrollo de software. De hecho, las mismas técnicas de depuración que se utilizaban hace 20 años se siguen utilizando ahora. A lo largo del tiempo, han surgido algunas alternativas, pero todavía queda un largo camino para que estas sean lo suficientemente útiles como para abrirse camino en el proceso de desarrollo de software. Una de ellas es la depuración algorítmica, la cual abstrae la información que el programador debe investigar para depurar el programa, permitiéndole de este modo centrarse en el qué está ocurriendo en vez de en el cómo. Esta abstracción tiene un coste: el nivel de granularidad de los errores que pueden detectarse nos permite como máximo aislar funciones mal implementadas, pero no averiguar qué parte de estas contiene el error. Esta tesis se centra en mejorar la depuración algorítmica en muchos aspectos. Concretamente, los principales objetivos de esta tesis son reducir el tiempo que el usuario necesita para detectar un error de programación así como proporcionar información más detallada de dónde se encuentra el error. Para conseguir estos objetivos, se han desarrollado técnicas para iniciar las sesiones de depuración lo antes posible, reducir el número de preguntas que se le van a realizar al usuario, y aumentar el nivel de granularidad de los errores que la depuración algorítmica puede detectar, permitiendo así seguir buscando el error incluso dentro de las funciones. Como resultado de esta tesis, se han definido tres técnicas completamente nuevas, se ha mejorado una técnica ya existente, y se han definido dos nuevas estrategias de depuración algorítmica que mejoran las previamente existentes. Además de los resultados teóricos, también se ha desarrollado un depurador algorítmico completamente funcional que contiene y respalda todas estas técnicas y estrategias. Este depurador está escrito en Java y depura código Java. La elección de este lenguaje se justifica debido a que es uno de los lenguajes más ampliamente extendidos y usados actualmente. También debido a que contiene una combinación interesante de retos todavía sin resolver para la depuración algorítmica. Para aumentar todavía más su usabilidad, el depurador ha sido posteriormente adaptado como un plugin de Eclipse, de tal manera que pudiese ser usado por un número más amplio de usuarios. Estos dos depuradores están públicamente disponibles para que cualquier persona interesada pueda acceder a ellos y continuar con la investigación si así lo deseara. / [CA] Hui en dia, els errors no detectats de programació suposen una despesa de milers de milions a l'any per a les empreses i institucions públiques i privades. Tot i això, no hi ha hagut cap avanç significatiu en l'àrea de la depuració que ajude als desenvolupadors durant la fase de desenvolupament de programari. De fet, les mateixes tècniques de depuració que s'utilitzaven fa 20 anys es continuen utilitzant ara. Al llarg del temps, han sorgit algunes alternatives, però encara queda un llarg camí perquè estes siguen prou útils com per a obrir-se camí en el procés de desenvolupament de programari. Una d'elles és la depuració algorítmica, la qual abstrau la informació que el programador ha d'investigar per a depurar el programa, permetent-li d'esta manera centrar-se en el què està ocorrent en compte de en el com. Esta abstracció té un cost: el nivell de granularitat dels errors que poden detectar-se ens permet com a màxim aïllar funcions mal implementades, però no esbrinar quina part d'estes conté l'error. Esta tesi es centra a millorar la depuració algorítmica en molts aspectes. Concretament, els principals objectius d'esta tesi són reduir el temps que l'usuari necessita per a detectar un error de programació així com proporcionar informació més detallada d'on es troba l'error. Per a aconseguir estos objectius, s'han desenvolupat tècniques per a iniciar les sessions de depuració com més prompte millor, reduir el nombre de preguntes que se li formularan a l'usuari, i augmentar el nivell de granularitat dels errors que la depuració algorítmica pot detectar, permetent així continuar buscant l'error inclús dins de les funcions. Com resultat d'esta tesi, s'han definit tres tècniques completament noves, s'ha millorat una tècnica ja existent, i s'han definit dos noves estratègies de depuració algorítmica que milloren les prèviament existents. A més dels resultats teòrics, també s'ha desenvolupat un depurador algorítmic completament funcional que conté i protegix totes estes tècniques i estratègies. Este depurador està escrit en Java i depura codi Java. L'elecció d'este llenguatge es justifica pel fet que és un dels llenguatges més àmpliament estesos i usats actualment. També pel fet que conté una combinació interessant de reptes encara sense resoldre per a la depuració algorítmica. Per a augmentar encara més la seua usabilitat, el depurador ha sigut posteriorment adaptat com un plugin d'Eclipse, de tal manera que poguera ser usat per un nombre més ampli d'usuaris. Estos dos depuradors estan públicament disponibles perquè qualsevol persona interessada puga accedir a ells i continuar amb la investigació si així ho desitjara. / Insa Cabrera, D. (2016). Optimization Techniques for Algorithmic Debugging [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/68506 / TESIS / Premios Extraordinarios de tesis doctorales

Esta tesis doctoral presenta un nuevo enfoque en el área de la transcripción musical automática (AMT), definiendo la tarea de Audio-to-Score (A2S), que realiza la transcripción musical de extremo a extremo gracias a la capacidad de modelado de problemas que nos ofrecen las redes neuronales profundas. Este enfoque va un paso más allá de los sistemas de transcripción tradicionales, que están basados en predecir notas musicales en el formato de tiempo-frecuencia llamado pianola o piano-roll en inglés. Las principales ventajas del enfoque propuesto frente a los métodos tradicionales son las siguientes: - La salida es una partitura válida de música que puede ser directamente interpretada por músicos o analizada por musicólogos. - La aproximación extremo a extremo evita que los errores de una etapa se propaguen a la siguiente. - No precisa de anotaciones de alineamiento temporal entre el audio de entrada y la partitura de salida, dado que se aprende por el modelo de forma implícita. - Mediante la aproximación extremo a extremo se aprende también un modelo de lenguaje musical que ayuda a reducir los errores de transcripción de manera global.

Tesis parcialmente patrocinada por la Conselleria de Cultura, Educació i Ciència de la Comunitat Valenciana y por el Ministerio de Ciencia y Tecnología (proyecto TIC2001-3530-C02-02)

No description available.

No description available.