Search

Esta obra es una contribución al campo de la Complejidad de la Demostración, que estudia la complejidad de los sistemas de demostración en términos de los recursos necesarios para demostrar o refutar fórmulas proposicionales. La Complejidad de la Demostración es un interesante campo relacionado con otros campos de la Informática como la Complejidad Computacional o la Demostración Automática entre otros. Esta obra se centra en medidas de complejidad para sistemas de demostración refutacionales para fórmulas en FNC. Consideramos varios sistemas de demostración, concretamente Resolución, R(k) y Planos Secantes y nuestros resultados hacen referencia a las medidas de complejidad de tamaño y espacio.Mejoramos separaciones de tamaño anteriores entre las versiones generales y arbóreas de Resolución y Planos Secantes. Para hacerlo, extendemos una cota inferior de tamaño para circuitos monótonos booleanos de Ran y McKenzie a circuitos monótonos reales. Este tipo de separaciones es interesante porque algunos demostradores automáticos se basan en la versión arbórea de sistemas de demostración, por tanto la separación indica que no es siempre una buena idea restringirnos a la versión arbórea.Tras la reciente aparición de R(k), que es un sistema de demostración entre Resolución y Frege con profundidad acotada, era importante estudiar cuan potente es y su relación con otros sistemas de demostración. Resolvemos un problema abierto propuesto por Krajícek, concretamente mostramos que R(2) no tiene la propiedad de la interpolación monónota factible. Para hacerlo, mostramos que R(2) es estrictamente más potente que Resolución.Una pregunta natural es averiguar si se pueden separar sucesivos niveles de R(k) o R(k) arbóreo. Mostramos separaciones exponenciales entre niveles sucesivos de lo que podemos llamar la jerarquía R(k) arbórea. Esto significa que hay formulas que requieren refutaciones de tamaño exponencial en R(k) arbóreo, pero tienen refutaciones de tamaño polinómico en R(k+1) arbóreo. Propusimos una nueva definición de espacio para Resolución mejorando la anterior de Kleine-Büning y Lettmann. Dimos resultados generales sobre el espacio para Resolución y Resolución arbórea y también una caracterización combinatoria del espacio para Resolución arbórea usando un juego con dos adversarios para fórmulas en FNC. La caracterización permite demostrar cotas inferiores de espacio para la Resolución arbórea sin necesidad de usar el concepto de Resolución o Resolución arbórea. Durante mucho tiempo no se supo si el espacio para Resolución y Resolución arbórea coincidían o no. Hemos demostrado que no coinciden al haber dado la primera separación entre el espacio para Resolución y Resolución arbórea.También hemos estudiado el espacio para R(k). Demostramos que al igual que pasaba con el tamaño, R(k) arbóreo también forma una jerarquía respecto alespacio. Por tanto, hay fórmulas que necesitan espacio casi lineal en R(k) arbóreo mientras que tienen refutaciones en R(k+1) arbóreo con espacio contante. Extendemos todas las cotas inferiores de espacio para Resolución conocidas a R(k) de una forma sencilla y unificada, que también sirve para Resolución, usando el concepto de satisfactibilidad dinámica presentado en esta obra., This work is a contribution to the field of Proof Complexity, which studies the complexity of proof systems in terms of the resources needed to prove or refute propositional formulas. Proof Complexity is an interesting field which has several connections to other fields of Computer Science like Computational Complexity or Automatic Theorem Proving among others. This work focuses in complexity measures for refutational proof systems for CNF formulas. We consider several proof systems, namely Resolution, R(k) and Cutting Planes and our results concern mainly to the size and space complexity measures. We improve previous size separations between treelike and general versions of Resolution and Cutting Planes. To do so we extend a size lower bound for monotone boolean circuits by Raz and McKenzie, to monotone real circuits. This kind of separations is interesting because some automated theorem provers rely on the treelike version of proof systems, so the separations show that is not always a good idea to restrict to the treelike version. After the recent apparition of R(k) which is a proof system lying between Resolution and bounded-depth Frege it was important to study how powerful it is and its relation with other proof systems. We solve an open problem posed by Krajícek, namely we show that R(2) does not have the feasible monotone interpolation property. To do so, we show that R(2) is strictly more powerful than Resolution. A natural question is to find out whether we can separate successive levels of R(k) or treelike R(k). We show exponential separations between successive levels of what we can call now the treelike R(k) hierarchy. That means that there are formulas that require exponential size treelike R(k) refutations whereas they have polynomial size treelike R(k+1) refutations. We have proposed a new definition for Resolution space improving a previous one from Kleine-Büning and Lettmann. We give general results for Resolution and treelike Resolution space and also a combinatorial characterization of treelike Resolution space via a Player-Adversary game over CNF formulas. The characterization allows to prove lower bounds for treelike Resolution space with no need to use the concept of Resolution or Resolution refutations at all. For a long time it was not known whether Resolution space and treelike Resolution space coincided or not. We have answered this question in the negative because we give the first space separation from Resolution to treelike Resolution. We have also studied space for R(k). We show that, as happened with respect to size, treelike R(k) forms a hierarchy respect to space. So, there are formulas that require nearly linear space for treelike R(k) whereas they have constant space treelike R(k+1) refutations. We extend all known Resolution space lower bounds to R(k) in an easier and unified way, that also holds for Resolution, using the concept of dynamical satisfiability introduced in this work.

La predicció és un concepte de recerca molt interessant. No es només predir el resultat futur, sinó que també cal predir el resultat conegut, a vegades anomenat validació. L'aplicació de tècniques de predicció sobre el comportament de sistemes és sempre molt útil perquè ens ajuda a comprendre el funcionament del elements que estem analitzant.Aquest treball va començar tot analitzant la influència de l'execució concurrent de diverses aplicacions de pas de missatges. Així, l'objectiu original era trobar i proposar uns algorismes de planificació de processos que obtinguessin un throughput màxim, equitatiu, i amb un rendiment adecuat del sistema.Per a poder avaluar adecuadament aquestes polítiques de planificació, varem trobar que ens calien eines d'analisi. Dimemas i Paraver són les eines de l'entorn que anomenem DiP. Tot i que aqueste eines varem estar dissenyades fa més de deu anys, són vàlides i ampliables.Dimemas es l'eina de predicció de rendiment. Tot fent ús de models senzills, pot predir el temps d'execució de les aplicacions de pas de missatges, fent servir un conjunt de paràmetres que modelitzen el funcionament del sistema. No és només una eina que prediu el temps d'execució, sinó que s'ha demostrat molt útil per entendre la influència dels diferents paràmetres del sistema en el temps de resposta de les aplicacionsL'eina d'anàlisi de l'entorn DiP s'anomena Paraver. Permet analitzar simultàniament moltes aplicacions i el sistema des de diferent punts de vista: analitzant els missatges, les contencions a la xarxa de comunicació, la planificació del processador.Promenvir/ST-ORM és l'eina d'anàlisi estocàstic. Inclou utilitats que permeten analitzar la influència de qualsevol paràmetre del sistema, així com sintonitzar els paràmetres de simulació, per aconseguir que les prediccions s'aproximin a la realitat.La qualitat i categoria de les decisions que varem prendre fa anys queda demostrada per la mètode de com cal utilitzar conjuntament totes les eines, i perquè són eines què es corresponen a l'estat de l'art actual.Aquest treball inclou la descripció de les diferents eines, des de el punt de vista de disseny fins la seva utilització (en cert grau), la validació de Dimemas, el disseny conceptual de Promenvir, la presentació del mètode que cal emprar amb aquestes eines (incloent anàlisi d'aplicacions individuals fins a anàlisis més complex), i alguns dels nostres primers anàlisi sobre polítiques de planificació de processador., Prediction is an interesting research topic. It is not only to predict the future result, but also to predict the past, often called validation. Applying prediction techniques to observed system behavior has always been extremely useful to understand the internals of the elements under analysis.We have started this work to analyze the influence of several message passing application when running in parallel. The original objective was to find and propose a process scheduling algorithm that maximizes the system throughput, fair, proper system utilization.In order to evaluate properly the different schedulers, it is necessary to use some tools. Dimemas and Paraver, conform the core of DiP environment. These tools has been designed ten years ago, but still valid and extensible.Dimemas is a performance prediction tool. Using a single models, it capable to predict execution time for message passing applications, considering few system parameters for the system. It is useful not only to predict the result of an execution, but to understand the influence of the system parameters in the execution time of the application.Paraver is the analysis tool of DiP environment. It allows the analysis of applications and system from several points of view: analyzing messages, contention in the interconnection network, processor scheduling.Promenvir/ST-ORM is a stochastic analysis tool. It incorporates facilities to analyze the influence of any parameter in the system, as well as to tune the simulation parameters, so the prediction is close to reality. The methodology on how to use these tools as a group to analyze the whole environment, and the fact that all those tools are State of the Art, demonstrates the quality of the decisions we made some years ago.This work includes description of the different tools, from its internal design to some external utilization, the validation of Dimemas, the concept design of Promenvir, the architecture for Promenvir, the presentation of the methodology used with these tools (for simple application analysis to complex system analysis), and some of our first analyses on processor scheduling policies.

The objective of this thesis is the development of algorithms for the simulation of the light transport in general environments to render high quality still images. To this end, first we have analyzed the existing methods able to render participating media, more concretely those that account for multiple scattering within the media. Next, we have devised a couple of two pass methods for the computation of those images. For the first step we have proposed algorithms to cope with the scenes we want to deal with. The second step uses the coarse solution of the first step to obtain the final rendered image.The structure of the dissertation is briefly presented below.In the first chapter the motivation of the thesis and its objectives are discussed. It also summarizes the contributions of the thesis and its organization.In the second chapter the principles of global illumination for general environments are reviewed, with the most important equations---the rendering equation and the transport equation---whose solution constitutes the global illumination problem. In order to solve the global illumination problem, a certain number of multi-pass methods exist. Their objective is to be able to skip restrictions on the number of types of light paths that could be dealt with a single technique, or increase efficiency and/or accuracy. We have opted to follow this philosophy, and a pair of two pass methods have been developed for general environments.The third chapter includes the study of the methods that perform the single scattering approximation, and also the study of the ones that take into account multiple scattering.The fourth chapter is devoted to our first pass method, which computes a rough estimate of the global illumination. Knowing the benefits of hierarchical approaches, two concrete algorithms based on hierarchies have been extended to be more generic: Hierarchical Radiosity with Clustering and Hierarchical Monte Carlo Radiosity.Our second pass is considered in the next chapter. Using the coarse solution obtained by the first pass, our second pass computes a high quality solution from a given viewpoint. Radiances and source radiances are estimated using Monte Carlo processes in the context of path tracing acceleration and also for final gather. Probability density functions (PDFs) are created at ray intersection points. For such a task, we initially used constant basis functions for the directional domain. After realizing of their limitations we proposed the Link Probabilities (LPs), which are objects with adaptive PDFs in the links-space.In order to take advantage of the effort invested for the construction of the LPs, we have devised two closely related progressive sampling strategies. In the second pass, instead of sampling each pixel individually, only a subset of samples is progressively estimated across the image plane. Our algorithms are inspired by the work of Michael D. McCool on anisotropic diffusion using conductance maps.The final chapter presents the conclusions of the thesis. Also possible lines of further research are suggested., El objetivo de esta tesis es el desarrollo de algoritmos para la simulación del transporte de la luz en los entornos genéricos para generar imágenes de la alta calidad. Con este fin, primero hemos analizado los métodos existentes capaces de visualizar medios participativos, más concretamente los que tienen en cuenta la dispersión múltiple en los medios. Después, hemos ideado un par de métodos de dos pasos para el cómputo de esas imágenes. Para el primer paso hemos propuesto algoritmos que hacen frente a las escenas que deseamos tratar. El segundo paso utiliza la solución aproximada del primer paso para obtener la imagen final. La estructura de la disertación se presenta brevemente en lo que sigue.En el primer capítulo se discuten la motivación de la tesis y sus objetivos. También se resumen las contribuciones de la tesis y su organización. En el segundo capítulo se repasan los principios de la iluminación global para los ambientes genéricos, con las ecuaciones-más importantes (la ecuación de rendering y la ecuación de transporte) cuya solución constituye el problema global de iluminación. Para solucionar el problema global de iluminación, cierto número de métodos de múltiples pasos existen. Su objetivo es poder eliminar restricciones en el número de tipos de caminos de luz que se podrían tratar con una sola técnica, o aumentar su eficacia y/o exactitud. Hemos optado seguir esta filosofía, desarrollando un par de métodos de dos pasos para entornos genéricos.El tercer capítulo incluye el estudio de los métodos que utilizan la aproximación de dispersión simple, y también el estudio de los que consideran la dispersión múltiple.El cuarto capítulo está dedicado a nuestro método de primer paso, que computa un cálculo aproximado de la iluminación global. Conociendo las ventajas de los métodos jerárquicos, dos algoritmos concretos basados en jerarquías se han ampliado para ser más genéricos: radiosidad jerárquica con clustering y radiosidad jerárquica usando Monte Carlo. Nuestro segundo paso se considera en el capítulo siguiente. Usando la solución aproximada obtenida por el primer paso, el segundo paso computa una solución de la alta calidad para un punto de vista dado. Se estiman las radiancias usando procesos de Monte Carlo en el contexto de la aceleración de trazadores de rayos y también para final gather. Las funciones de densidad de probabilidad (PDFs) se crean en los puntos de interacción de los rayos. Para tal tarea, utilizamos inicialmente funciones constantes como base para el dominio direccional. Después de comprender sus limitaciones, propusimos establecer probabilidades directamente sobre los enlaces (link probabilities, o LPs), usando objetos con PDFs adaptativos en el espacio de los enlaces.Para aprovechar el esfuerzo invertido en la construcción de los LPs, hemos ideado dos estrategias de muestreo progresivas. En el segundo paso, en vez de muestrear cada pixel individualmente, solamente se estima progresivamente un subconjunto de muestras a través del plano de imagen. Nuestros algoritmos han sido inspirados en el trabajo de Michael D. McCool en la difusión anisotrópica usando mapas de conductancia.El capítulo final presenta las conclusiones de la tesis, y también sugiere las líneas posibles de investigación futura.

Aquesta tesi presenta una nova metodologia per resoldre problemes de presa de decisions. Hemestudiat els casos en què cal considerar més d'un criteri. Aquests tipus de mètodes de decisió esconeixen com MCDM (Multiple Criteria Decision Making), o també MCDA (Multiple CriteriaDecision Aid). La diferència entre simplement "prendre decisions" o "ajudar a prendredecisions" recau en si el mètode es dissenya per recomanar la decisió a prendre o si tambéinclou elements que permeten entendre com es prenen les decisions en un cert context. La nostraproposta inclou elements dels dos plantejaments. D'una banda, hem intentat que la persona queha d'usar el mètode no necessiti aprendre tècniques complexes abans de poder-lo aplicar a casosreals. D'altra banda, el mètode no és una caixa negra, sinó que l'usuari rep informació sobrecaracterístiques de les dades que ha de tenir en compte abans de fer la decisió final.ClusDM és un mètode de presa de decisions pensat per resoldre dos tipus concrets deproblemes: (i) ordenar un conjunt d'alternatives de la millor a la pitjor, (ii) seleccionar lesmillors alternatives del conjunt. La dificultat d'aquest procés recau en que cal maximitzardiversos criteris parcials (i normalment no correlacionats) al mateix temps. A la tesi es pottrobar un resum de les diferents aproximacions a aquest tipus de problemes de decisió. Nomésdestacar que el nostre mètode segueix les bases de la Teoria de la Utilitat.Els mètodes clàssics consideren només criteris numèrics. Diferents extensions a aquests modelss'han anat desenvolupant durant els últims anys. En aquesta tesis ens hem plantejat lapossibilitat de tenir criteris que utilitzin diferents tipus de valors. A més, hem afegit dues fases ala metodologia habitual (que té una fase d'agregació i una d'ordenació), que són: l'explicaciódel resultat i l'avaluació de la qualitat.La "Fase d'explicació" està dedicada a assignar un terme lingüístic per descriure cadaalternativa segons la seva posició en el ranking. L'ús de vocabularis qualitatius facilita lacomprensió del resultat. El significat dels diferents termes usats ve donat per una funció denegació. Aquesta representació es basa en contrastar el significat d'un terme amb el dels termesoposats (els seus antònims).La "Fase d'Avaluació de la Qualitat" analitza a fons els resultats intermedis obtinguts en elsdiferents passos del procés i intenta mesurar l'error acumulat. ClusDM proporciona diversesmesures de qualitat parcial per cada fase del procés, de manera que l'usuari tingui constància dela confiança que pot donar al resultat final que doni el sistema., This thesis presents a new methodology for decision making. In particular, we have studied theproblems that consider more than one criterion, which is known as Multiple Criteria DecisionMaking (MDCM) or Multiple Criteria Decision Aid (MCDA). The difference relies on the factof imitating the behaviour of the decision maker (i.e. develop a method that makes decisions) orgiving to the decision maker some additional information that allows him to understand themechanism of solving decisions (i.e. the decision maker can learn from the use of the method).Our proposal fits better in the MCDA approach, but has also similarities with the MCDMperspective. On one hand, the method we have designed is independent enough to not require adeep understanding of the process by the decision maker. On the other hand, we have carefullystudied the process and the method is able to extract knowledge about the decision problem,which is given to the user to let him know any special characteristics of the data analysed.ClusDM is a new method to solve multicriteria decision problems. It is able to find a ranking ofalternatives or to select the best ones. This process is not easy since usually it is not possible tomaximise all the partial profits (i.e.criteria) at the same time. In the thesis we present anoverview of the large amount of methods developed to solve this problem. We follow the utilitytheory approach.Classical methods consider only numerical criteria. Some extensions allow the consideration ofother scales, such as, fuzzy or ordinal values, but usually they are required to have a commonscale for all criteria. This thesis faces the problem of managing different types of criteria at thesame time. Methods following the utility approach consider two steps to sort a decisionproblem out: the aggregation and the ranking. We have included some additional steps in orderto improve the process: (i) the explanation phase and (ii) the quality measurement phase.In the "Explanation Phase", special attention is devoted to give an appropriate linguisticdescription of the ranking. The necessity to give a qualitatively described result has been arguedby different authors. The rationale behind this belief is that human decision makers understandbetter a linguistic statement characterising the selected alternative (or ranking of alternatives)than a numerical result or even a membership function. In this context, a new negation-basedsemantics has been studied. The key idea is that we can infer the meaning of a term knowing theterms that express an opposite value. The use of this new semantics representation seemsappropriate to obtain a result that can be easily understood by the decision maker.In the "Quality Measurement Phase", different quality measures for each stage of the processare calculated. With these measures we can give an overall value of the trustworthiness of thefinal result. This kind of information is very useful for the decision maker in order to pay moreor less attention to the recommendations of the system.

Les contribucions d'aquesta tesi uneixen dues disciplines: ciències ambientals (específicament, gestió d'aigües residuals) i informàtica (específicament, intel·ligència artificial). El tractament d'aigües residuals com a disciplina opera fent servir un rang de diferents enfocaments i mètodes que inclouen: control manual, control automàtic on-line, modelat numèric o no-numèric, models estadístics i simulacions. La tesi caracteritza la recerca interdisciplinària de tècniques d'intel·ligència artificial (raonament basat en regles, raonament basat en casos, ontologies i planificació) a sistemes de suport a la decisió a l'entorn ambiental. El disseny de l'arquitectura d'aquesta aplicació, el sistema OntoWEDSS, augmenta els sistemes clàsics de raonament existents (raonament basat en regles i basat en casos) amb una ontologia de domini per a la gestió de plantes de tractament d'aigües residuals. La integració de l'ontologia WaWO recentment creada proporciona a OntoWEDSS una major flexibilitat en la capacitat de gestió. La construcció del sistema de suport a la decisió OntoWEDSS es basa en l'estudi d'un cas específic, però el sistema també és d'interès general ja que l'arquitectura basada en l'ontologia pot aplicar-se a qualsevol estació depuradora i, a un nivell apropiat d'abstracció, a altres dominis ambientals. El sistema OntoWEDSS millora la diagnosi de l'estat de l'estació depuradora, proporciona suport a la solució de complexes problemes relacionats amb aigües residuals, i facilita el modelatge del coneixement i la seva reutilització mitjançant l'ontologia WaWO. En particular, a la investigació s'han aconseguit els següents objectius: (1) la millora del modelatge de la informació sobre processos de tractament d'aigües residuals i la clarificació de part de la confusió existent en la terminologia del domini, (2) la incorporació de coneixement microbiològic (referent al procés del tractament i modelat mitjançant una ontologia) dins del procés de raonament, (3) la creació d'un sistema de suport a la decisió amb tres nivells (percepció, diagnosi i suport a la decisió) que combina coneixement mitjançant una nova integració entre KBSs i ontologies, proporcionant millors resultats, (4) la eliminació d'obstacles existents en el raonament, obtinguda utilitzant el nou coneixement microbiològic codificat a l'estructura jeràrquica i a les relacions de l'ontologia, (5) la representació de relacions causa-efecte, degut a la implementació d'un conjunt de relacions que permeten a l'ontologia deduir automàticament la resposta a qüestions sobre el domini d'aigües residuals. OntoWEDSS està implementada en el llenguatge de programació LISP, fent servir el software Allegro Common LISP. S'ha dut a terme una avaluació focalitzada del sistema, basada en la valoració de la capacitat de resposta a situacions problemàtiques específiques, obtenint-se bons resultats., Las contribuciones de esta tesis unen dos disciplinas: ciencias ambientales (específicamente, gestión de aguas residuales) e informática (específicamente, inteligencia artificial). El tratamiento de aguas residuales como disciplina opera utilizando un rango de diferentes enfoques y métodos que incluye: control automático on-line, modelado numérico o no-numérico, razonamiento basado en reglas, razonamiento basado en casos, soporte a la decisión y planificación. La tesis caracteriza una aplicación interdisciplinaria de técnicas de inteligencia artificial a sistemas de soporte a la decisión en el dominio ambiental. El diseño de la arquitectura de esta aplicación, el sistema OntoWEDSS, aumenta los sistemas híbridos de razonamiento ya existentes (razonamiento basado en reglas y basado en casos) con una ontología de dominio para la gestión de plantas de tratamiento de aguas residuales. La integración de la ontología WaWO, de nueva creación, proporciona a OntoWEDSS una mayor flexibilidad en la capacidad de gestión. La construcción del sistema de soporte a la decisión OntoWEDSS se basa en el estudio de un caso específico, pero el sistema resulta también es de interés general puesto que la arquitectura basada en ontologías puede aplicarse a cualquier planta de tratamiento de aguas residuales y, a un nivel apropiado de abstracción, a otros dominios ambientales. El sistema OntoWEDSS mejora la diagnosis del estado de la planta de tratamiento, proporciona soporte a la resolución de complejos problemas relacionados con aguas residuales, y facilita el modelado del conocimiento y su reutilización mediante la ontología WaWO. En particular, la investigación ha alcanzado los siguientes objetivos: (1) la mejora del modelado de la información sobre procesos de tratamiento de aguas residuales y la clarificación de parte de la confusión existente en la terminología relacionada, (2) la incorporación de conocimiento microbiológico (referente al proceso del tratamiento y modelado mediante una ontología) dentro del proceso de razonamiento, (3) la creación de un sistema de soporte a la decisión con tres estratos (percepción, diagnosis y soporte a la decisión) que combina conocimiento mediante una novedosa integración entre KBSs y ontologías, proporcionando mejores resultados, (4) la eliminación de obstáculos existentes en el razonamiento, hallada utilizando el nuevo conocimiento microbiológico codificado en la estructura jerárquica y las relaciones de la ontología, (5) la representación de relaciones causa-efecto, debido a la implementación de un conjunto de relaciones que permiten a la ontología deducir automáticamente la respuesta a cuestiones sobre el dominio de aguas residuales. OntoWEDSS está implementada en el lenguaje de programación LISP, usando el software Allegro Common LISP. Se ha llevado a cabo una evaluación enfocada del sistema, basada en la valoración de la capacidad de respuesta a situaciones problemáticas específicas, obteniéndose buenos resultados., The contributions of this thesis bridge two disciplines: environmental science (specifically, wastewater management) and computer science (specifically, artificial intelligence). Wastewater management as a discipline operates using a range of different approaches and methods which include: manual control, on-line automatic control, numerical or non-numerical models, statistical models and simulation models. The thesis characterizes an interdisciplinary research on artificial intelligence techniques (rule-based reasoning, case-based reasoning, ontologies and planning) applied to environmental decision-support systems. The integrated architecture's design of this application, the OntoWEDSS system, augments classic reasoning systems (rule-based reasoning and case-based reasoning) with a domain ontology about the management of wastewater treatment plants. The integration of the newly created WaWO ontology provides a more flexible management capability to OntoWEDSS. The construction of the OntoWEDSS decision support system is based on a specific case study but the system is also of general interest, given that its ontology-underpinned architecture can be applied to any wastewater treatment plant and, at an appropriate level of abstraction, to other environmental domains. The OntoWEDSS system improves the diagnosis of the state of a treatment plant, provides support for wastewater-related complex problem-solving, and facilitates knowledge modeling and reuse by means of the WaWO ontology. The following research targets have been achieved in particular: (1) the improvement of the modeling of the information about wastewater treatment processes and the clarification of a part of the existing terminological confusion in the domain, (2) the incorporation of ontology-modeled microbiological knowledge related to the treatment process into the reasoning process, (3) the creation of a decision support system with three layers (perception, diagnosis and decision support) which combines knowledge through a novel integration between KBSs and ontologies, providing better results, (4) the solution of existing reasoning-impasses, found using the new microbiological knowledge encoded in the hierarchical structure and the relations of the ontology, (5) the representation of cause-effect relations, due to the implementation of a set of relations that enable the ontology to automatically deduce the answer to questions about the wastewater domain. OntoWEDSS is implemented in the LISP programming language, using Allegro Common LISP software. A focused evaluation of the system, founded on the assessment of the capacity of response to specific problematic situations, has been carried out and has given fine results., Questa tesi contribuisce alla intersezione di due discipline: le scienze ambientali (specificamente, la gestione delle acque di rifiuto) e la informatica (specificamente, la intelligenza artificiale). Nel trattamento delle acque di rifiuto come disciplina si utilizzano diversi metodi, che includono: controllo manuale, controllo automatico on-line, modelli numerici o non-numerici e simulazioni. La tesi caratterizza un'applicazione interdisciplinare di tecniche di intelligenza artificiale a sistemi di aiuto alla decisione in campo ambientale. L'architettura di questa applicazione, il sistema OntoWEDSS, amplia i sistemi di ragionamento ibrido esistenti (ragionamento basato su un sistema di regole, ragionamento basato sull'esperienza, aiuto alla decisione e pianificazione) con un'ontologia di dominio per la gestione di depuratori di acque di rifiuto. L'integrazione dell'ontologia WaWO, di nuova creazione, fornisce a OntoWEDSS una maggiore flessibilità nella sua capacità di gestione. La costruzione del sistema OntoWEDSS si basa sullo studio di un caso specifico, però il sistema risulta anche di interesse generale dato che l'architettura basata su un'ontologia può essere applicata a un qualsiasi depuratore e, considerando un adeguato livello d'astrazione, ad altri domini ambientali. Il sistema OntoWEDSS migliora la diagnosi dello stato del depuratore, fornisce aiuto alla soluzione di problemi complessi relazionati con le acque di rifiuto e facilita la modellizzazione della conoscenza e la sua riutilizzazione mediante l'ontologia WaWO. In particolare, la ricerca realizzata ha raggiunto i seguenti obiettivi: (1) il miglioramento dell'informazione sui processi di depurazione e il chiarimento di parte della confusione esistente nella terminologia relativa, (2) l'incorporazione di conoscenza microbiologica (riguardo al processo di depurazione e mediante la modellizzazione ontologica) nel processo di ragionamento, (3) la creazione di un sistema di aiuto alla decisione con tre livelli (percezione, diagnosi e aiuto alla decisione) che combina la informazione mediante un nuovo tipo d'integrazione tra classici sistemi basati sulla conoscenza e ontologie, proporzionando risultati migliori, (4) l'eliminazione di alcuni ostacoli esistenti nel ragionamento, ottenuta utilizzando la nuova conoscenza microbiologica codificata nella struttura gerarchica e nelle relazioni dell'ontologia, (5) la rappresentazione di relazioni causa-effetto del mondo reale attraverso l'implementazione di un insieme di relazioni ontologiche che permettono di dedurre automaticamente le risposte a domande sul dominio delle acque di rifiuto. OntoWEDSS è implementata nel linguaggio di programmazione LISP, usando il software Allegro Common LISP. È stata realizzata una valutazione del sistema basata sulla stima della capacità di risposta a situazioni problematiche specifiche e si sono ottenuti risultati soddisfacenti.

A TYPE -THEORETIC APPROACH TO PROOF SUPPORT FOR ALGEBRAIC DESIGN FRAMEWORKS En el desarrollo formal de software, la especificación formal se utiliza con fines de verificación y validación. Se han definido diferentes tipos de especificaciones formales. En esta tesis nos centraremos en especificaciones algebraicas. Este tipo de especificaciones formales son especificaciones axiomáticas, que suelen definirse en un lenguaje de especificación que incluye diferentes operadores de estructuración. La semántica de estos operadores se define de una forma que sea lo más independiente posible de la lógica de especificación o institución. Otra etapa fundamental en métodos formales es el diseño de software. Las tareas básicas que suelen realizarse durante esta etapa son la deducción de propiedades a partir de una especificación, el refinamiento de especificaciones o verificar que un programa satisface una especificación. Entendemos por entorno de diseño algebraico a un formalismo que incluye la definición de un lenguaje de especificación algebraica con semántica formal y la definición implícita o explícita de, al menos, las dos primeras de las tres tareas de diseño mencionadas anteriormente. Es importante que la definición de los entornos de diseño algebraico sea tambien lo más independiente posible de la lógica del lenguaje de especificación y, si es el caso, que la definición sea para una clase arbitraria de lenguajes de programación. El entorno de diseño algebraico con el que trabajaremos en esta tesis está basado en un lenguaje de especificación muy sencillo que ha sido utilizado para dar semántica a otros lenguajes de especificación de más alto nivel. El principal objetivo de esta tesis es definir un marco formal que permite reusar demostradores de teoremas para teorías de tipos con tipos dependientes e inductivos para el desarrollo de demostradores de teoremas para entornos de diseño algebraico. El problema puede considerarse interesante por varios motivos. Primero, esperamos que el desarrollo de este tipo de herramientas incrementará el uso de este tipo de métodos formales. Segundo, la investigación a realizar es completamente diferente a los trabajos realizados anteriormente y por último, el trabajo requiere un conocimiento extenso de una familia de formalismos no standard que forman las diferentes teorías de tipos con tipos dependientes que se han definido. En esta tesis, primero presentamos de forma general, las características basicas y las aplicaciones de las diferentes teorías de tipos con tipos dependientes. Estudiamos con más detalle la teoría de tipos que vamos a utilizar en el resto de la tesis, y a continuación presentamos un nuevo principio de codificación de sistemas de demostración finitos para la teoría de tipos escogida que mejora algunas de las limitaciones de otros principios de codificación existentes.Con el fin de comparar de forma abstracta las diferentes semánticas dadas a ciertos operadores de comportamiento del lenguaje de especificación escogido, definimos una institución a la que denominamos institución algebraica de comportamiento. Esta institución es también útil para definir las formas normales de las especificaciones que son necesarias para definir cierta clase de sistemas de demostración. A continuación, presentamos diferentes sistemas de demostración para la deducción de propiedades a partir de especificaciones y para el refinamiento de especificaciones. La principal aportación en esta parteconsiste en rediseñar los sistemas de demostración que no es posible dar representaciones adecuadas en la teoría de tipos escogida por ser sistemas de demostración infinitarios.Finalmente, damos una representación en la teoría de tipos de los sistemas de demostración más significativos de nuestro entorno de diseño algebraico usando el nuevo principio de codificación presentado en la tesis. Esto nos permite reutilizar los demostradores de teoremas de la teoría de tipos escogida para el desarrollo de demostradores de teoremas del entorno de diseño algebraico escogido. A TYPE -THEORETIC APPROACH TO PROOF SUPPORT FOR ALGEBRAIC DESIGN FRAMEWORKSIn software engineering, a formal specification of what a system has to do plays a crucial role in the software development process. Formality is required for verification and validation purposes. Different forms of formal specifications have been developed. This thesis concentrates on the algeraic approach to system specification. In essence, this approach can be characterized by:· Axiomatic specifications which consist of a signature together with a set of axioms in a specification logic which any implementation of the system with that specification has to satisfy.· Operations to combine and modify specifications from subspecifications with an algebraic semantics.· An abstract presentation of the semantics as independent as possible of the specification logic or institution.Another crucial step in the software development process is software design. Some of the usual tasks which are performed during software design are the following: deduction of properties from specifications, refinement of specifications and verification of a program with respect to a specification. We understand by an algebraic design framework a formalism which includes a formal definition of an algebraic specification language including a model-theoretic semantics and the implicit or explicit formal definition of at least the two first software design tasks. The definition of algebraic design frameworks should be for several specification logics or even better for an arbitrary but fixed institution, and if it is the case for an arbitrary class of programming languages. In the literature, there exists a large amount of algebraic specification languages and algebraic design frameworks. The algebraic design framework which we will work in this thesis will be based on a kernel and simple algebraic specification language. The main objective of this thesis is to give an approach to reuse theorem provers for type theories with dependent and inductive types for the development of theorem provers for algebraic design frameworks. The problem can be considered interesting for several reasons. First, we believe that the development of tools in type-theoretic theorem provers will help to spread the use of algebraic techniques. Note that these kind of theorem provers have been widely used and applied. Second, the work to be done is completely different to the work done before and finally this work requires a thorough understanding of a non-standard family of formalisms which are type theories. In this thesis, first we give an overall view of type theories together with their apllications and then we present a new principle of encoding in an expressive type theory which solves some of the limitations of previous principle of encodings. In order to give a generic presentation of the framework of ASL for different specification logics, we give an abstract semantic framework in which the semantics of the the behavioural operators of ASL can be uniformly instantiated in first-order and higher-order logic. We also redesign the different proof systems for deduction and refinement when it is not possible to give adequate encodings in the type theory because they are infinatary proof systems. In some cases, different solutions are given for first and higher-order logics. Finally, the main proof systems of the algebraic design framework for ASL have been encoded in UTT using the new principle of encoding presented in the thesis. This allows us to take advantage of the current implementation of theorem provers for UTT to implement proof checkers for the proof systems of our chosen algebraic design framework.

de la tesi doctoralL'objectiu principal del treball realitzat ha sigut el desenvolupar una manera de modelar el procés d'investigació racional (l'evolució de les creences d'un agent racional com a conseqüència de la seva interacció amb l'entorn i dels seus procesos d'inferència), mantenint la idea general del model dels móns possibles i la semàntica de Kripke, però intentant evitar els problemes de l'omnisciència lògica i el raonament ideal. Les contribucions principals del treball són:· S'ha fet un estudi molt detallat sobre les diferents propostes que s'han fet en el tema del tractament formal del problema de l'omnisciència lògica en les lògiques modals de creences. Aquest estudi ressalta les semblances i diferències entre les diverses solucions i mostra fins a quin punt solucionen el problema del raonament ideal.· Com a resultat d'aquest estudi, es suggereix una nova aproximació al problema, basada en el concepte dels móns impossibles. La idea principal és que una situació pot ser percebuda de diferents maneres per diferents agents; així, una situació pot ser descrita de forma subjectiva per cadascun d'ells. A més, en cada situació un agent pot tenir raons per recolzar i/o rebutjar determinats fets. La percepció que un agent té del seu entorn determina les seves creences en aquella situació. Aquestes són les idees bàsiques del concepte de situacions subjectives proposat a la tesi.· S'ha determinat quines són les activitats bàsiques que poden modificar les creences d'un agent racional (realització de deduccions, plantejament de dubtes, plantejament de preguntes a l'entorn i rebuda de dades externes). També s'ha definit una classe específica d'agents racionals, els investigadors racionals, que realitzen aquestes activitats d'una forma concreta (manipulant fórmules de primer ordre en un arbre de taulers analítics).· Per últim, a la tesi es mostra com l'evolució de les creences dels investigadors racionals, causada per la seva anàlisi dinàmica multi-dimensional, pot ser modelitzada formalment dins del marc de les situacions subjectives. Això es fa utilitzant les situacions concebibles, que corresponen a aquells escenaris que l'agent pot considerar, independenment de la seva possible parcialitat o inconsistència. L'evolució de les creences d'un agent es modelitza amb la generació d'una seqüència de relacions d'accessibilitat, en la que, després de cada pas d'anàlisi de les creences, van canviant les situacions concebibles considerades com a alternatives viables per l'agent., of the PhD thesisThe main aim of this work has been to develop a way to model the process of rational inquiry (the evolution of a rational agent's set of beliefs over time as a consequence of its interaction with the world and its internal inferential processes), keeping the general idea of the possible worlds model and the Kripke semantics but trying to avoid the problems of logical omniscience and perfect reasoning. The actual contributions of the work described in the thesis are the following:· An extensive survey of the state of the art has been made, in which the most relevant approaches that have been proposed to solve the problems of logical omniscience and perfect reasoning are presented. This review focuses on the similarities and differences between the various solutions and shows to which degree they provide a framework in which it is possible to model non-ideal reasoners.· As a result of this study, an impossible-worlds based framework in which logical omniscience is avoided is suggested. The main idea of this proposal is that a situation may be perceived in different ways by different agents; thus, a situation may be described subjectively by each of them. Furthermore, in each situation an agent may have reasons to suport and/or reject certain facts. The perception that an agent has of a situation will determine its beliefs in that situation. These are the basic ideas underlying the subjective situations described in the dissertation.· It has been determined which are the basic activities that may modify the set of beliefs of a rational agents (performing deductions, posing doubts, making questions to the environment and receiving external data). A specific class of rational agents, called rational inquirers, is also defined. These agents perform their doxastic activities in a concrete way, which is based in the manipulation of first-order formulae contained in an analytic tableaux tree. · Finally, in the dissertation it is shown how the evolution of the beliefs of the rational inquirers, caused by their dynamic multi-dimensional analysis, may be formally modelled in the subjective situations framework. This modelling is performed using conceivable situations, which correspond to those scenarios that may be considered by the modelled agent, irrespective of their possible partiality or inconsistency. The evolution of the beliefs of an agent is modelled with the generation of a sequence of accessibility relations in which, after each step of belief analysis, the situations that are considered as viable by the agent change in an appropriate way.

The thesis describes the application of the relaxation labelling algorithm to NLP disambiguation. Language is modelled through context constraint inspired on Constraint Grammars. The constraints enable the use of a real value statind "compatibility". The technique is applied to POS tagging, Shallow Parsing and Word Sense Disambigation. Experiments and results are reported. The proposed approach enables the use of multi-feature constraint models, the simultaneous resolution of several NL disambiguation tasks, and the collaboration of linguistic and statistical models., La tesi descriu l'aplicació de l'algorisme d'etiquetat per relaxacio (relaxation labelling) a la desambiguació del llenguatge natural. La llengua es modela mitjançant restriccions de context inspirades en les Constraint Grammars. Les restriccions permeten l'ús d'un valor real que n'expressa la "compatibilitat". La tècnica s'aplica a la desambiguació morfosintàctica (POS tagging), a l'anàlisi sintàctica superficial (Shallow Parsing) i a la desambiguació semàntica (Word Sense Disambigation), i se'n presenten experiments i resultats. L'enfoc proposat permet la utilització de models de restriccions amb trets múltiples, la resolució simultània de diverses tasques de desambiguació del llenguatge natural, i la col·laboració de models linguístics i estadístics.