Maximality principles such as the ones going back to Kuratowski and Zorn ensure the existence of higher type ideal objects the use of which is commonly held indispensable for mathematical practice. The modern turn towards computational methods, which can be witnessed to have a strong influence on contemporary foundational studies, encourages a reassessment within a constructive framework of the methodological intricacies that go along with invocations of maximality principles. The common thread that can be followed through the chapters of this thesis is explained by the attempt to put the widespread use of ideal objects under constructive scrutiny. It thus walks the tracks of a revised Hilbert’s programme which has inspired a reapproach to constructive algebra by finitary means, and for which Scott’s entailment relations have already shown to provide a vital and utmost versatile tool. In this thesis several forms of the Kuratowski-Zorn Lemma are introduced and proved equivalent over constructive set theory; the notion of Jacobson radical is brought from commutative rings to a general ideal theory for single-conclusion entailment relations; a flexible conservation criterion of Scott for multi-conclusion entailment relations is put into action; elementary and constructive variants for algebraic extension theorems such as Sikorski’s on the injectivity of complete atomic Boolean algebras are phrased and proved in terms of entailment relations; and a point-free version of Sikora’s theorem on spaces of orderings of groups is obtained by a revisitation with syntactical means of some of the classical criteria for groups to be orderable.

In this PhD thesis we study the extended-order algebras and their properties; moreover, we evaluate the possibility to apply them in other mathematical contexts, as, for instance, the fuzzy implicators and the many-valued relations.

This thesis is concerned with the study of nonstandard models in measure theory and in functional analysis. In measure theory, we define elementary numerosities, that are additive measures that take on values in a non-archimedean field and for which the measure of every singleton is 1. We have shown that, by taking the ratio with a suitable unit of measurement, from a numerosity it can be defined a non-atomic real-valued measure, and that every non-atomic measure can be obtained from a numerosity by this procedure. We then used numerosities to develop a model for the probability of infinite sequences of coin tosses coherent with the original ideas of Laplace. In functional analysis, we introduce a space of functions of nonstandard analysis with a formally finite domain, that extends both the space of distributions and the space of Young measures. Among the applications of this space of functions, we develop a continuous-in-time, discrete-in-space nonstandard formulation for a class of ill-posed forward-backward parabolic equations, and on the study of the regularity and asymptotic behaviour of its nonstandard solutions. This approach proved to be a viable alternative to the study of the vanishing viscosity limit of the solution of a pseudoparabolic regularization of the original problem.

In this thesis, we study the problem of reasoning and query answering over contextualized knowledge in quad format augmented with expressive forall-existential bridge rules. Such bridge rules contain conjunctions, existentially quantified variables in the head, and are strictly more expressive than the bridge rules considered so far in similar setting. A set of quads together with forall-existential bridge rules is called a quad-system. We show that query answering over quad-systems in their unrestricted form is undecidable, in general. We propose various subclasses of quad-systems, for which query answering is decidable. Context-acyclic quad-systems do not allow the context dependency graph of the bridge rules to have cycles passing through triple-generating (value-generating) contexts, and hence guarantees the chase (deductive closure) to be finite. Csafe, msafe and safe classes of quad-systems restricts the structure of descendance graph of Skolem blank nodes generated during chase process to be directed acyclic graphs (DAGs) of bounded depth, and hence has finite chases. RR and restricted RR quad-systems do not allow for the creation of Skolem blank nodes, and hence restrict the chase to be of polynomial size. Besides the undecidability result of unrestricted quad-systems, tight complexity bounds has been established for each of the classes we have introduced. We then compare the problems, (resp. classes,) we address (resp. derive) in this thesis, for quad-systems with analogous problems (resp. classes) in the realm of forall-existential rules. We show that the query answering problem over quad-systems is polynomially equivalent to the query answering problem over ternary forall-existential rules, and the technique of safety, we propose, is strictly more expressive than existing well known techniques such joint acyclicity and model maithful acyclicity, used for decidability guarantees, in the realm of forall-existential rules.

Many projects have dealt with mappings between classifications both in computer science and digital library communities. The adopted solutions range from fully manual to fully automatic approaches. Manual approaches are very precise, but automation becomes unavoidable when classifications contain thousands of nodes with millions of candidate correspondences. As fun-damental preliminary step towards automation, S-Match converts classifications into formal on-tologies, i.e. lightweight ontologies. Despite many solutions to the problem have been offered, with S-Match representing a state of the art matcher with good accuracy and run-time perfor-mance, there are still several open problems. In particular, the problems addressed in this thesis include: (a) Run-time performance. Due to the high number of calls to the SAT reasoning engine, semantic matching may require exponential time; (b) Maintenance. Current matching tools offer poor support to users for the process of creation, validation and maintenance of the correspond-ences; (c) Lack of background knowledge. The lack of domain specific background knowledge is one important cause of low recall. As significant progress to (a) and (b), we describe MinSMatch, a semantic matching tool we developed evolving S-Match that computes the minimal mapping between two lightweight ontologies. The minimal mapping is that minimal subset of correspondences such that all the others can be efficiently computed from them and are therefore said to be redundant. We provide a formal definition of minimal and, dually, redundant map-pings, evidence of the fact that the minimal mapping always exists and it is unique and a correct and complete algorithm for computing it. Our experiments demonstrate a substantial improve-ment in run-time. Based on this, we also developed a method to support users in the validation task that allows saving up to 99% of the time. We address problem (c) by creating and by making use of an extensible diversity-aware knowledge base providing a continuously growing quantity of properly organized knowledge. Our approach is centered on the fundamental notions of domain and context. Domains, developed by adapting the faceted approach from library science, are the main means by which diversity is captured and allow scaling as with them it is possible to add new knowledge as needed. Context allows a better disambiguation of the terms used and re-ducing the complexity of reasoning at run-time. As proof of the applicability of the approach, we developed the Space domain and applied it in the Semantic Geo-Catalogue (SGC) project.

Description Logics (DLs) are a family of logic-based knowledge representation formalisms aimed at representing the knowledge of an application domain in a structured way one of whose main characteristic is the emphasis on reasoning. Since the last two decades Description logics have been widely studied and applied to numerous areas of computer science (including artificial intelligence, formal verification, database theory, natural language processing and distributed computing). In recent years, however, the interest in the problem of automated reasoning in Description Logics has seen a tremendous growth because of the explosion of new notable applications in the domains of Semantic Web and of bio-medical ontologies. The more real-world problems are represented through DL-based ontologies the more these new applications represents a challenge due to the required efficiency in handling complex logical constructors (e.g. numerical constraints) and in handling the huge dimensions of this kind of ontologies. For these reasons the development of efficient algorithms and procedures for reasoning in Description Logic has become crucial. SAT-based technologies, in the meanwhile, proved to be mature and largely successful in many other automated reasoning fields, first of all on many very hard practical applications of formal verification, often huge characterized by problems of huge dimension. In the last twenty years, in fact, we have witnessed an impressive advance in the efficiency of SAT techniques, which has brought problems of hundreds of millions of clauses and variables to be at the reach of the freely-available state-of-the-art solvers. As a consequence, many problems have been successfully solved by mean of SAT-based techniques and these approaches are currently state-of-the-art in the respective communities (among all Model Checking). Furthermore, the progress in SAT-solving techniques, together with the concrete needs from real applications, have inspired significant research on richer and more expressive Boolean formalism, like Satisfiability Modulo Theories (SMT), and on the use of the SAT formalism to solve problems with a wider extent (e.g. to compute interpolants, unsatisfiable cores, all-SAT). The research trends in Description Logic, its manifold practical applications, the quest of efficient and scalable procedures, on one hand, the wide variety of mature and efficient techniques offered by the SAT research area, on the other hand, motivated our research. In this thesis dissertation we explore the idea of exploiting the power and efficiency of state-of-the-art SAT-based techniques for automated reasoning and ontology manipulation in Description Logics, proposing a convenient alternative to the traditional tableau based algorithms. With this aim we propose and develop novel and complete approaches able to solve Description Logic problems as SAT and SMT ones, by mean of sound and complete encodings. On these encodings we develop new procedures and optimizations techniques based on a variety of existing SAT-based formalisms and technologies. In this work, in particular, we focus on three gradually harder reasoning problems in Description Logics which tackle increasingly more expressive languages or increasingly harder reasoning services, among which we face also non-standard services supporting the debugging of ontologies like modularization and axiom pinpointing. We implemented our approaches in tools which integrate with the available SAT/SMT-solvers; finally, we show the effectiveness of our novel approaches through very extensive empirical evaluations on benchmarks and ontologies from real application, in which we compare our performance against the other state-of-the-art available systems. Notice that any advance in the exploited Boolean reasoning techniques/tools will be freely inherited from our proposed approaches extending also to Description Logics/ontologies the benefits of the observable great and fast advance in the efficiency of SAT-based techniques.

Assuring safety and reliability is fundamental when developing a safety critical system. Road, naval and avionic transportation; water and gas distribution; nuclear, eolic, and photovoltaic energy production are only some examples where it is mandatory to guarantee those properties. The continuous increasing in the design complexity of safety critical system calls for a never ending sought of new and more advanced analytical techniques. In fact, they are required to assure that undesired consequences are highly improbable. In this Thesis we introduce a novel methodology able to raise the bar in the area of automated safety and reliability analysis. The proposed approach integrates a series of techniques, based on symbolic model checking, into the current development process of safety critical systems. Moreover, our methodology and the resulting techniques are thereafter applied to a series of real-world case studies, developed in collaboration with authoritative entities such as NASA and the Boeing Company.

The underlying idea of the Semantic Web is that web content should be expressed not only in natural language but also in a language that can be unambiguously understood, interpreted and used by software agents, thus permitting them to find, share and integrate information more easily. The central notion of the Semantic Web's syntax are ontologies, shared vocabularies providing taxonomies of concepts, objects and relationships between them, which describe particular domains of knowledge. A vocabulary stores words, synonyms, word sense definitions (i.e. glosses), relations between word senses and concepts; such a vocabulary is generally referred to as the Controlled Vocabulary (CV) if choice or selection of terms are done by domain specialists. A facet is a distinct and dimensional feature of a concept or a term that allows a taxonomy, ontology or CV to be viewed or ordered in multiple ways, rather than in a single way. The facet is clearly defined, mutually exclusive, and composed of collectively exhaustive properties or characteristics of a domain. For example, a collection of rice might be represented using a name facet, place facet etc. This thesis presents a methodology for producing mappings between Controlled Vocabularies, based on a technique called \Hidden Semantic Matching". The \Hidden" word stands for it not relying on any sort of externally provided background knowledge. The sole exploited knowledge comes from the \semantic context" of the same CVs which are being matched. We build a facet for each concept of these CVs, considering more general concepts (broader terms), less general concepts (narrow terms) or related concepts (related terms).Together these form a concept facet (CF) which is then used to boost the matching process.

Escoamentos multifásicos em meios porosos são modelados por um sistema de equações diferenciais parciais e o estudo da aproximação das soluções dessas equações desempenha papel crucial na simulação e previsão de problemas de grande interesse prático e impacto econômico e social, tais como a recuperação secundária de petróleo, o armazenamento geológico de CO2 e o transporte de poluentes em aquíferos. O presente trabalho tem como objetivo o desenvolvimento de um simulador numérico tridimensional para avaliar com precisão o transporte de dois fluidos imiscíveis em um meio poroso heterogêneo e que utiliza computação paralela multithread para computadores multiprocessados de memória compartilhada. O sistema de equações diferenciais parciais é decomposto em um subsistema elíptico para a determinação do campo de velocidades dos fluidos e uma equação hiperbólica não-linear para o transporte das fases fluidas. Para esta última, foi utilizado um método numérico de volumes finitos, não-oscilatório de alta ordem baseado em esquemas centrais e que admite uma formulação semi-discreta com coeficientes variáveis no espaço. Experimentos numéricos em modelos tridimensionais foram realizados considerando problemas de escoamentos lineares e não lineares postos em configurações típicas de simulação de reservatórios de petróleo. Os resultados mostraram-se satisfatórios por apresentarem conservação da massa, boa captura das ondas de choque e pequena difusão numérica, independente do passo de tempo. / Multiphase flows in porous media are modeled by a system of partial differential equations and the study of the numerical approximation to the solutions of these plays a crucial role in the simulation and prediction of problems that are of great practical interest and of economic and social impact, such as secondary oil recovery, geological storage of CO2 and transport of pollutants in aquifers. The goal of this work is the development of a three-dimensional numerical simulator that precisely evaluates the transport of two immiscible fluids in a heterogeneous porous media using multithread parallel programming to shared memory multiprocessors computers. The system of partial differential equations is decomposed into a elliptic subsystem used to determine the velocity field and into a hyperbolic equation (nonlinear) to determine the transport of the fluid phases. The approximation to the solution of the latter one is calculated using a high order non-oscillatory finite-differences numerical method based on central schemes that allows a semi-discrete formulation which an extension that enables to work with variable space coefficients. Numerical experiments on three-dimensional models were performed considering linear and nonlinear flow problems in typical settings of oil reservoirs simulations. The results were satisfactory since they presented mass conservation, precise capture of shock waves and small numeric diffusion, regardless of the time step.

A tomada de decisÃo à um processo cognitivo que conduz à seleÃÃo de um plano de escolha dentre vÃrios. Este pode ser concebido atravÃs do juÃzo de um ou vÃrios indivÃduos, os quais serÃo definidos como agentes. O trabalho em questÃo terà como cerne ambientes onde grupo de indivÃduos atuam simultaneamente influenciando uns aos outros, ou seja, iremos trabalhar com sistemas multiagentes. Dentre a classe de problemas envolvidos pela tomada de decisÃo, destacam-se os Problemas de DecisÃo MulticritÃrio. Estes sÃo uma variaÃÃo dos Problemas de DecisÃo usuais onde a correta tomada de decisÃo se processa atravÃs da apreciaÃÃo de vÃrios critÃrios, os quais sÃo utilizados para descrever o objeto/fato a ser decidido. Para que seja possÃvel a tomada de decisÃo, se faz necessÃrio uma estratÃgia que analise o problema em questÃo, de modo a determinar as alternativas sobre as quais o tomador de decisÃo deverà escolher, avalie cada critÃrio que compÃe a alternativa, diante dos possÃveis valores que estes podem assumir, para, assim, realizar a tomada de decisÃo. Dentre as diversas estratÃgias utilizadas para resolver este tipo de problemas, destacam-se aquelas que usam a LÃgica MatemÃtica como tÃcnica de modelagem e soluÃÃo. Amplamente estudada por pesquisadores vinculados à InteligÃncia Artificial, a LÃgica MatemÃtica utiliza-se de conceitos especÃficos de sua sintaxe e semÃntica para modelar ambientes complexos e estabelecer por mÃtodos especÃficos a tomada de decisÃo. Dentre as abordagens relevantes vinculadas à LÃgica MatemÃtica, destacam-s aquelas que empregam a LÃgica de Primeira Ordem. Inspirado nas LÃgica de PreferÃncias clÃssicas, este trabalho propÃe a LÃgica de Primeira Ordem para problemas de DecisÃo com AgregaÃÃo de PreferÃncias FODPA. Esta à capaz de modelar e resolver Problemas de DecisÃo MulticritÃrio em ambientes multiagentes atravÃs de tÃcnicas relacionadas Ãs LÃgicas com AgregaÃÃo de PreferÃncias e à LÃgica de Primeira Ordem. / Decision making is a cognitive procedure that lead to selection of a plan of choice among several. This can be designed through the judgment of one or more individuals, who are defined as agents. The work in question will have as core environments where several individuals act simultaneously, that is, we will work with multi-agent systems. Among the problems involved by the decision making processes, stand out the Multicriteria Decision Problems. These are a variation of the usual Decision Problems where the correct decision-making processes through the assessment of various criteria, which are used to describe the object / fact to be decided. To be able the correct decision making, a strategy is necessery to analyze the problem, determine the alternatives on which the decision maker must choose, evaluate each criterion that compose an alternative towards the possible values that each criterion can assume, thus, take the decision. Among the several strategies used to solve such problems, stand out those that use the Mathematical Logic as modeling and solution techniques. Extensively studied by researchers in Artificial Intelligence, the Mathematical Logic uses specific concepts of its syntax and semantics to model complex environments and establish decision-making. Inspired by the Classical Preferences Logics, this work aims to propose the First Order Logic for Decison problems with Preference Aggregation {FODPA}. This is able to model and solve Multicriteria Decisiom Problems in multi-agent environments by techniques related to Preferences Logics and the First Order Logic.