语义网的一阶逻辑推理技术支持

研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.

一阶逻辑中约束求解的局部搜索法

以一阶谓词逻辑为基础，讨论约束满足问题．着重研究一阶逻辑公式可满足性的局部搜索法，并与命题逻辑中的可满足性过程加以比较．以皇后问题和哈密顿回路问题为例，说明基于一阶逻辑的方法能处理较大的问题实例．

An Infinite Pebble Game and Applications

We generalize the well-known pebble game to infinite dag's, and we use this generalization to give new and shorter proofs of results in different areas of computer science (as diverse as "logic of programs" and "formal language theory"). Our applications here include a proof of a theorem due to Salomaa, asserting the existence of a context-free language with infinite index, and a proof of a theorem due to Tiuryn and Erimbetov, asserting that unbounded memory increases the power of logics of programs. The original proofs by Salomaa, Tiuryn, and Erimbetov, are fairly technical. The proofs by Tiuryn and Erimbetov also involve advanced techniques of model theory, namely, back-and-forth constructions based on a variant of Ehrenfeucht-Fraisse games. By contrast, our proofs are not only shorter, but also elementary. All we need is essentially finite induction and, in the case of the Tiuryn-Erimbetov result, the compactness and completeness of first-order logic.

Fred: An approach to generating real, correct, reusable programs from proofs

In this paper we describe our system for automatically extracting "correct" programs from proofs using a development of the Curry-Howard process. Although program extraction has been developed by many authors, our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique to reduce higher-order logic to many-sorted (first-order) logic; 2. the free use of new rules for induction subject to certain conditions; 3. the extensive use of previously programmed (total, recursive) functions; 4. the use of templates to make the reasoning much closer to normal mathematical proofs and 5. a conceptual distinction between the computational type theory (for representing programs)and the logical type theory (for reasoning about programs). As an example of our system we give a constructive proof of the well known theorem that every graph of even parity, which is non-trivial in the sense that it does not consist of isolated vertices, has a cycle. Given such a graph as input, the extracted program produces a cycle as promised.

Um modelo algébrico para a lógica do muito

Pós-graduação em Filosofia - FFC

Aspectos lógicos e algébricos dos conjuntos fuzzy

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

A lógica do muito em um sistema de tablôs

Pós-graduação em Filosofia - FFC

Inconsistent-tolerant base revision through Argument Theory Change

Reasoning and change over inconsistent knowledge bases (KBs) is of utmost relevance in areas like medicine and law. Argumentation may bring the possibility to cope with both problems. Firstly, by constructing an argumentation framework (AF) from the inconsistent KB, we can decide whether to accept or reject a certain claim through the interplay among arguments and counterarguments. Secondly, by handling dynamics of arguments of the AF, we might deal with the dynamics of knowledge of the underlying inconsistent KB. Dynamics of arguments has recently attracted attention and although some approaches have been proposed, a full axiomatization within the theory of belief revision was still missing. A revision arises when we want the argumentation semantics to accept an argument. Argument Theory Change (ATC) encloses the revision operators that modify the AF by analyzing dialectical trees-arguments as nodes and attacks as edges-as the adopted argumentation semantics. In this article, we present a simple approach to ATC based on propositional KBs. This allows to manage change of inconsistent KBs by relying upon classical belief revision, although contrary to it, consistency restoration of the KB is avoided. Subsequently, a set of rationality postulates adapted to argumentation is given, and finally, the proposed model of change is related to the postulates through the corresponding representation theorem. Though we focus on propositional logic, the results can be easily extended to more expressive formalisms such as first-order logic and description logics, to handle evolution of ontologies.

Sobre la compatibilidad entre realismo y relativismo conceptual : Un exámen de la tesis de Putnam, desde un punto de vista lógico

Las indagaciones en la pregunta por lo que hay permiten distinguir a grandes rasgos entre dos enfoques: uno, el de los pensadores que entendieron que el tema a investigar era la naturaleza y estructura del mundo, y otro, el de aquellos quienes, al sostener que describir el mundo no es simplemente copiarlo, atendieron a lo que se llamó esquema conceptual: esto es, al marco conceptual cuya forma toman las descripciones del mundo. La situación se puede plantear como un dilema, ninguno de cuyos cuernos permite alentar esperanzas de avances bien fundados. O bien se pretende describir el mundo, tal como es, sin contemplar el hecho de que esa descripción incluye elecciones conceptuales propias de un sujeto, o bien se centra la investigación en los rasgos de el/los esquema/s conceptual/es imprescindibles para construir una descripción del mundo, imposibilitando, con ello, el acceso a la realidad tal como ésta es. En el siglo XX se cuenta con recursos de sistemas de lógica considerablemente más desarrollados y abarcadores (en sus posibilidades de aplicación) que los anteriores. Tales recursos brindan nuevas posibilidades de abordaje de la pregunta por lo que hay, no sólo por los ámbitos que se clarifican mediante ellos, sino también por el sustento que ofrecen para la reflexión filosófica los resultados obtenidos. Los avances producidos en el ámbito de la lógica en algo más de un siglo tuvieron variadas repercusiones en el enfoque y el tratamiento de distintas cuestiones filosóficas. Así, se ha echado mano a conceptos y recursos de lógica al considerar preguntas acerca de la estructura del mundo. Para la determinación de los componentes de la realidad se ha recurrido a la lógica, desde diversas posiciones filosóficas. Por ejemplo, se ha entendido que la lógica subyacente a la teoría científica brinda en algún sentido elementos para determinar la ontología (o para descartar la posibilidad de hacerlo, o para establecer qué función cumple la noción de ontología en la teoría científica). También, desde una óptica más amplia, se ha intentado mostrar que el uso del lenguaje tiene consecuencias respecto de la ontología. Hilary Putnam ha sugerido la posibilidad de ser al mismo tiempo un realista y un relativista conceptual. Involucra consideraciones como las mencionadas, respecto de lógica y ontología. Su objetivo es el intento de hacer justicia a la realidad y al misterio de nuestro mundo de sentido común. Tomo esta tesis como una propuesta de trabajo. Me interesa pensar en cómo ofrecer algunos elementos de juicio para evaluar sus alcances. Para ello, examino la sugerencia de Putnam mediante un ejemplo construido con ese objetivo. Entiendo que se requerirán, al menos, dos esquemas conceptuales diferentes: al que surgiría de la lógica de orden 1, tal como la desarrolla Quine, y al que podría obtenerse a partir de la teoría de objetos no existentes de Castañeda. Se contará así con elementos de juicio más precisos que los habituales para evaluar las consecuencias que se seguirían para la ontología en caso de sostener ambos esquemas conceptuales, en consonancia con la propuesta de Putnam que se ha tomado como objetivo general del proyecto

Sobre la compatibilidad entre realismo y relativismo conceptual : Un exámen de la tesis de Putnam, desde un punto de vista lógico

Las indagaciones en la pregunta por lo que hay permiten distinguir a grandes rasgos entre dos enfoques: uno, el de los pensadores que entendieron que el tema a investigar era la naturaleza y estructura del mundo, y otro, el de aquellos quienes, al sostener que describir el mundo no es simplemente copiarlo, atendieron a lo que se llamó esquema conceptual: esto es, al marco conceptual cuya forma toman las descripciones del mundo. La situación se puede plantear como un dilema, ninguno de cuyos cuernos permite alentar esperanzas de avances bien fundados. O bien se pretende describir el mundo, tal como es, sin contemplar el hecho de que esa descripción incluye elecciones conceptuales propias de un sujeto, o bien se centra la investigación en los rasgos de el/los esquema/s conceptual/es imprescindibles para construir una descripción del mundo, imposibilitando, con ello, el acceso a la realidad tal como ésta es. En el siglo XX se cuenta con recursos de sistemas de lógica considerablemente más desarrollados y abarcadores (en sus posibilidades de aplicación) que los anteriores. Tales recursos brindan nuevas posibilidades de abordaje de la pregunta por lo que hay, no sólo por los ámbitos que se clarifican mediante ellos, sino también por el sustento que ofrecen para la reflexión filosófica los resultados obtenidos. Los avances producidos en el ámbito de la lógica en algo más de un siglo tuvieron variadas repercusiones en el enfoque y el tratamiento de distintas cuestiones filosóficas. Así, se ha echado mano a conceptos y recursos de lógica al considerar preguntas acerca de la estructura del mundo. Para la determinación de los componentes de la realidad se ha recurrido a la lógica, desde diversas posiciones filosóficas. Por ejemplo, se ha entendido que la lógica subyacente a la teoría científica brinda en algún sentido elementos para determinar la ontología (o para descartar la posibilidad de hacerlo, o para establecer qué función cumple la noción de ontología en la teoría científica). También, desde una óptica más amplia, se ha intentado mostrar que el uso del lenguaje tiene consecuencias respecto de la ontología. Hilary Putnam ha sugerido la posibilidad de ser al mismo tiempo un realista y un relativista conceptual. Involucra consideraciones como las mencionadas, respecto de lógica y ontología. Su objetivo es el intento de hacer justicia a la realidad y al misterio de nuestro mundo de sentido común. Tomo esta tesis como una propuesta de trabajo. Me interesa pensar en cómo ofrecer algunos elementos de juicio para evaluar sus alcances. Para ello, examino la sugerencia de Putnam mediante un ejemplo construido con ese objetivo. Entiendo que se requerirán, al menos, dos esquemas conceptuales diferentes: al que surgiría de la lógica de orden 1, tal como la desarrolla Quine, y al que podría obtenerse a partir de la teoría de objetos no existentes de Castañeda. Se contará así con elementos de juicio más precisos que los habituales para evaluar las consecuencias que se seguirían para la ontología en caso de sostener ambos esquemas conceptuales, en consonancia con la propuesta de Putnam que se ha tomado como objetivo general del proyecto

Sobre la compatibilidad entre realismo y relativismo conceptual : Un exámen de la tesis de Putnam, desde un punto de vista lógico

Las indagaciones en la pregunta por lo que hay permiten distinguir a grandes rasgos entre dos enfoques: uno, el de los pensadores que entendieron que el tema a investigar era la naturaleza y estructura del mundo, y otro, el de aquellos quienes, al sostener que describir el mundo no es simplemente copiarlo, atendieron a lo que se llamó esquema conceptual: esto es, al marco conceptual cuya forma toman las descripciones del mundo. La situación se puede plantear como un dilema, ninguno de cuyos cuernos permite alentar esperanzas de avances bien fundados. O bien se pretende describir el mundo, tal como es, sin contemplar el hecho de que esa descripción incluye elecciones conceptuales propias de un sujeto, o bien se centra la investigación en los rasgos de el/los esquema/s conceptual/es imprescindibles para construir una descripción del mundo, imposibilitando, con ello, el acceso a la realidad tal como ésta es. En el siglo XX se cuenta con recursos de sistemas de lógica considerablemente más desarrollados y abarcadores (en sus posibilidades de aplicación) que los anteriores. Tales recursos brindan nuevas posibilidades de abordaje de la pregunta por lo que hay, no sólo por los ámbitos que se clarifican mediante ellos, sino también por el sustento que ofrecen para la reflexión filosófica los resultados obtenidos. Los avances producidos en el ámbito de la lógica en algo más de un siglo tuvieron variadas repercusiones en el enfoque y el tratamiento de distintas cuestiones filosóficas. Así, se ha echado mano a conceptos y recursos de lógica al considerar preguntas acerca de la estructura del mundo. Para la determinación de los componentes de la realidad se ha recurrido a la lógica, desde diversas posiciones filosóficas. Por ejemplo, se ha entendido que la lógica subyacente a la teoría científica brinda en algún sentido elementos para determinar la ontología (o para descartar la posibilidad de hacerlo, o para establecer qué función cumple la noción de ontología en la teoría científica). También, desde una óptica más amplia, se ha intentado mostrar que el uso del lenguaje tiene consecuencias respecto de la ontología. Hilary Putnam ha sugerido la posibilidad de ser al mismo tiempo un realista y un relativista conceptual. Involucra consideraciones como las mencionadas, respecto de lógica y ontología. Su objetivo es el intento de hacer justicia a la realidad y al misterio de nuestro mundo de sentido común. Tomo esta tesis como una propuesta de trabajo. Me interesa pensar en cómo ofrecer algunos elementos de juicio para evaluar sus alcances. Para ello, examino la sugerencia de Putnam mediante un ejemplo construido con ese objetivo. Entiendo que se requerirán, al menos, dos esquemas conceptuales diferentes: al que surgiría de la lógica de orden 1, tal como la desarrolla Quine, y al que podría obtenerse a partir de la teoría de objetos no existentes de Castañeda. Se contará así con elementos de juicio más precisos que los habituales para evaluar las consecuencias que se seguirían para la ontología en caso de sostener ambos esquemas conceptuales, en consonancia con la propuesta de Putnam que se ha tomado como objetivo general del proyecto

Semantic Service Discovery Techniques for the composable web

This PhD thesis contributes to the problem of resource and service discovery in the context of the composable web. In the current web, mashup technologies allow developers reusing services and contents to build new web applications. However, developers face a problem of information flood when searching for appropriate services or resources for their combination. To contribute to overcoming this problem, a framework is defined for the discovery of services and resources. In this framework, three levels are defined for performing discovery at content, discovery and agente levels. The content level involves the information available in web resources. The web follows the Representational Stateless Transfer (REST) architectural style, in which resources are returned as representations from servers to clients. These representations usually employ the HyperText Markup Language (HTML), which, along with Content Style Sheets (CSS), describes the markup employed to render representations in a web browser. Although the use of SemanticWeb standards such as Resource Description Framework (RDF) make this architecture suitable for automatic processes to use the information present in web resources, these standards are too often not employed, so automation must rely on processing HTML. This process, often referred as Screen Scraping in the literature, is the content discovery according to the proposed framework. At this level, discovery rules indicate how the different pieces of data in resources’ representations are mapped onto semantic entities. By processing discovery rules on web resources, semantically described contents can be obtained out of them. The service level involves the operations that can be performed on the web. The current web allows users to perform different tasks such as search, blogging, e-commerce, or social networking. To describe the possible services in RESTful architectures, a high-level feature-oriented service methodology is proposed at this level. This lightweight description framework allows defining service discovery rules to identify operations in interactions with REST resources. The discovery is thus performed by applying discovery rules to contents discovered in REST interactions, in a novel process called service probing. Also, service discovery can be performed by modelling services as contents, i.e., by retrieving Application Programming Interface (API) documentation and API listings in service registries such as ProgrammableWeb. For this, a unified model for composable components in Mashup-Driven Development (MDD) has been defined after the analysis of service repositories from the web. The agent level involves the orchestration of the discovery of services and contents. At this level, agent rules allow to specify behaviours for crawling and executing services, which results in the fulfilment of a high-level goal. Agent rules are plans that allow introspecting the discovered data and services from the web and the knowledge present in service and content discovery rules to anticipate the contents and services to be found on specific resources from the web. By the definition of plans, an agent can be configured to target specific resources. The discovery framework has been evaluated on different scenarios, each one covering different levels of the framework. Contenidos a la Carta project deals with the mashing-up of news from electronic newspapers, and the framework was used for the discovery and extraction of pieces of news from the web. Similarly, in Resulta and VulneraNET projects the discovery of ideas and security knowledge in the web is covered, respectively. The service level is covered in the OMELETTE project, where mashup components such as services and widgets are discovered from component repositories from the web. The agent level is applied to the crawling of services and news in these scenarios, highlighting how the semantic description of rules and extracted data can provide complex behaviours and orchestrations of tasks in the web. The main contributions of the thesis are the unified framework for discovery, which allows configuring agents to perform automated tasks. Also, a scraping ontology has been defined for the construction of mappings for scraping web resources. A novel first-order logic rule induction algorithm is defined for the automated construction and maintenance of these mappings out of the visual information in web resources. Additionally, a common unified model for the discovery of services is defined, which allows sharing service descriptions. Future work comprises the further extension of service probing, resource ranking, the extension of the Scraping Ontology, extensions of the agent model, and contructing a base of discovery rules. Resumen La presente tesis doctoral contribuye al problema de descubrimiento de servicios y recursos en el contexto de la web combinable. En la web actual, las tecnologías de combinación de aplicaciones permiten a los desarrolladores reutilizar servicios y contenidos para construir nuevas aplicaciones web. Pese a todo, los desarrolladores afrontan un problema de saturación de información a la hora de buscar servicios o recursos apropiados para su combinación. Para contribuir a la solución de este problema, se propone un marco de trabajo para el descubrimiento de servicios y recursos. En este marco, se definen tres capas sobre las que se realiza descubrimiento a nivel de contenido, servicio y agente. El nivel de contenido involucra a la información disponible en recursos web. La web sigue el estilo arquitectónico Representational Stateless Transfer (REST), en el que los recursos son devueltos como representaciones por parte de los servidores a los clientes. Estas representaciones normalmente emplean el lenguaje de marcado HyperText Markup Language (HTML), que, unido al estándar Content Style Sheets (CSS), describe el marcado empleado para mostrar representaciones en un navegador web. Aunque el uso de estándares de la web semántica como Resource Description Framework (RDF) hace apta esta arquitectura para su uso por procesos automatizados, estos estándares no son empleados en muchas ocasiones, por lo que cualquier automatización debe basarse en el procesado del marcado HTML. Este proceso, normalmente conocido como Screen Scraping en la literatura, es el descubrimiento de contenidos en el marco de trabajo propuesto. En este nivel, un conjunto de reglas de descubrimiento indican cómo los diferentes datos en las representaciones de recursos se corresponden con entidades semánticas. Al procesar estas reglas sobre recursos web, pueden obtenerse contenidos descritos semánticamente. El nivel de servicio involucra las operaciones que pueden ser llevadas a cabo en la web. Actualmente, los usuarios de la web pueden realizar diversas tareas como búsqueda, blogging, comercio electrónico o redes sociales. Para describir los posibles servicios en arquitecturas REST, se propone en este nivel una metodología de alto nivel para descubrimiento de servicios orientada a funcionalidades. Este marco de descubrimiento ligero permite definir reglas de descubrimiento de servicios para identificar operaciones en interacciones con recursos REST. Este descubrimiento es por tanto llevado a cabo al aplicar las reglas de descubrimiento sobre contenidos descubiertos en interacciones REST, en un nuevo procedimiento llamado sondeo de servicios. Además, el descubrimiento de servicios puede ser llevado a cabo mediante el modelado de servicios como contenidos. Es decir, mediante la recuperación de documentación de Application Programming Interfaces (APIs) y listas de APIs en registros de servicios como ProgrammableWeb. Para ello, se ha definido un modelo unificado de componentes combinables para Mashup-Driven Development (MDD) tras el análisis de repositorios de servicios de la web. El nivel de agente involucra la orquestación del descubrimiento de servicios y contenidos. En este nivel, las reglas de nivel de agente permiten especificar comportamientos para el rastreo y ejecución de servicios, lo que permite la consecución de metas de mayor nivel. Las reglas de los agentes son planes que permiten la introspección sobre los datos y servicios descubiertos, así como sobre el conocimiento presente en las reglas de descubrimiento de servicios y contenidos para anticipar contenidos y servicios por encontrar en recursos específicos de la web. Mediante la definición de planes, un agente puede ser configurado para descubrir recursos específicos. El marco de descubrimiento ha sido evaluado sobre diferentes escenarios, cada uno cubriendo distintos niveles del marco. El proyecto Contenidos a la Carta trata de la combinación de noticias de periódicos digitales, y en él el framework se ha empleado para el descubrimiento y extracción de noticias de la web. De manera análoga, en los proyectos Resulta y VulneraNET se ha llevado a cabo un descubrimiento de ideas y de conocimientos de seguridad, respectivamente. El nivel de servicio se cubre en el proyecto OMELETTE, en el que componentes combinables como servicios y widgets se descubren en repositorios de componentes de la web. El nivel de agente se aplica al rastreo de servicios y noticias en estos escenarios, mostrando cómo la descripción semántica de reglas y datos extraídos permiten proporcionar comportamientos complejos y orquestaciones de tareas en la web. Las principales contribuciones de la tesis son el marco de trabajo unificado para descubrimiento, que permite configurar agentes para realizar tareas automatizadas. Además, una ontología de extracción ha sido definida para la construcción de correspondencias y extraer información de recursos web. Asimismo, un algoritmo para la inducción de reglas de lógica de primer orden se ha definido para la construcción y el mantenimiento de estas correspondencias a partir de la información visual de recursos web. Adicionalmente, se ha definido un modelo común y unificado para el descubrimiento de servicios que permite la compartición de descripciones de servicios. Como trabajos futuros se considera la extensión del sondeo de servicios, clasificación de recursos, extensión de la ontología de extracción y la construcción de una base de reglas de descubrimiento.

Analysis of service-oriented computing systems

La computación basada en servicios (Service-Oriented Computing, SOC) se estableció como un paradigma ampliamente aceptado para el desarollo de sistemas de software flexibles, distribuidos y adaptables, donde las composiciones de los servicios realizan las tareas más complejas o de nivel más alto, frecuentemente tareas inter-organizativas usando los servicios atómicos u otras composiciones de servicios. En tales sistemas, las propriedades de la calidad de servicio (Quality of Service, QoS), como la rapídez de procesamiento, coste, disponibilidad o seguridad, son críticas para la usabilidad de los servicios o sus composiciones en cualquier aplicación concreta. El análisis de estas propriedades se puede realizarse de una forma más precisa y rica en información si se utilizan las técnicas de análisis de programas, como el análisis de complejidad o de compartición de datos, que son capables de analizar simultáneamente tanto las estructuras de control como las de datos, dependencias y operaciones en una composición. El análisis de coste computacional para la composicion de servicios puede ayudar a una monitorización predictiva así como a una adaptación proactiva a través de una inferencia automática de coste computacional, usando los limites altos y bajos como funciones del valor o del tamaño de los mensajes de entrada. Tales funciones de coste se pueden usar para adaptación en la forma de selección de los candidatos entre los servicios que minimizan el coste total de la composición, basado en los datos reales que se pasan al servicio. Las funciones de coste también pueden ser combinadas con los parámetros extraídos empíricamente desde la infraestructura, para producir las funciones de los límites de QoS sobre los datos de entrada, cuales se pueden usar para previsar, en el momento de invocación, las violaciones de los compromisos al nivel de servicios (Service Level Agreements, SLA) potenciales or inminentes. En las composiciones críticas, una previsión continua de QoS bastante eficaz y precisa se puede basar en el modelado con restricciones de QoS desde la estructura de la composition, datos empiricos en tiempo de ejecución y (cuando estén disponibles) los resultados del análisis de complejidad. Este enfoque se puede aplicar a las orquestaciones de servicios con un control centralizado del flujo, así como a las coreografías con participantes multiples, siguiendo unas interacciones complejas que modifican su estado. El análisis del compartición de datos puede servir de apoyo para acciones de adaptación, como la paralelización, fragmentación y selección de los componentes, las cuales son basadas en dependencias funcionales y en el contenido de información en los mensajes, datos internos y las actividades de la composición, cuando se usan construcciones de control complejas, como bucles, bifurcaciones y flujos anidados. Tanto las dependencias funcionales como el contenido de información (descrito a través de algunos atributos definidos por el usuario) se pueden expresar usando una representación basada en la lógica de primer orden (claúsulas de Horn), y los resultados del análisis se pueden interpretar como modelos conceptuales basados en retículos. ABSTRACT Service-Oriented Computing (SOC) is a widely accepted paradigm for development of flexible, distributed and adaptable software systems, in which service compositions perform more complex, higher-level, often cross-organizational tasks using atomic services or other service compositions. In such systems, Quality of Service (QoS) properties, such as the performance, cost, availability or security, are critical for the usability of services and their compositions in concrete applications. Analysis of these properties can become more precise and richer in information, if it employs program analysis techniques, such as the complexity and sharing analyses, which are able to simultaneously take into account both the control and the data structures, dependencies, and operations in a composition. Computation cost analysis for service composition can support predictive monitoring and proactive adaptation by automatically inferring computation cost using the upper and lower bound functions of value or size of input messages. These cost functions can be used for adaptation by selecting service candidates that minimize total cost of the composition, based on the actual data that is passed to them. The cost functions can also be combined with the empirically collected infrastructural parameters to produce QoS bounds functions of input data that can be used to predict potential or imminent Service Level Agreement (SLA) violations at the moment of invocation. In mission-critical applications, an effective and accurate continuous QoS prediction, based on continuations, can be achieved by constraint modeling of composition QoS based on its structure, known data at runtime, and (when available) the results of complexity analysis. This approach can be applied to service orchestrations with centralized flow control, and choreographies with multiple participants with complex stateful interactions. Sharing analysis can support adaptation actions, such as parallelization, fragmentation, and component selection, which are based on functional dependencies and information content of the composition messages, internal data, and activities, in presence of complex control constructs, such as loops, branches, and sub-workflows. Both the functional dependencies and the information content (described using user-defined attributes) can be expressed using a first-order logic (Horn clause) representation, and the analysis results can be interpreted as a lattice-based conceptual models.

Semantic reasoning for autonomic IT systems

Autonomic systems are required to adapt continually to changing environments and user goals. This process involves the real-Time update of the system's knowledge base, which should therefore be stored in a machine-readable format and automatically checked for consistency. OWL ontologies meet both requirements, as they represent collections of knowl- edge expressed in FIrst order logic, and feature embedded reasoners. To take advantage of these OWL ontology char- acteristics, this PhD project will devise a framework com- prising a theoretical foundation, tools and methods for de- veloping knowledge-centric autonomic systems. Within this framework, the knowledge storage and maintenance roles will be fulfilled by a specialised class of OWL ontologies. ©2014 ACM.

Methods for Solving Necessary Equivalences

Nonmonotonic Logics such as Autoepistemic Logic, Reflective Logic, and Default Logic, are usually defined in terms of set-theoretic fixed-point equations defined over deductively closed sets of sentences of First Order Logic. Such systems may also be represented as necessary equivalences in a Modal Logic stronger than S5 with the added advantage that such representations may be generalized to allow quantified variables crossing modal scopes resulting in a Quantified Autoepistemic Logic, a Quantified Autoepistemic Kernel, a Quantified Reflective Logic, and a Quantified Default Logic. Quantifiers in all these generalizations obey all the normal laws of logic including both the Barcan formula and its converse. Herein, we address the problem of solving some necessary equivalences containing universal quantifiers over modal scopes. Solutions obtained by these methods are then compared to related results obtained in the literature by Circumscription in Second Order Logic since the disjunction of all the solutions of a necessary equivalence containing just normal defaults in these Quantified Logics, is equivalent to that system.