Many ontologies, in particular in the biomedical domain, are based on the Description Logic EL++. Several efforts have been made to interpret and exploit EL++ontologies by distributed representation learning. Specifically, concepts within EL++theories have been represented as n-balls within an n-dimensional embedding space. However, the intersectional closure is not satisfied when using n-balls to represent concepts because the intersection of two n-balls is not an n-ball. This leads to challenges when measuring the distance between concepts and inferring equivalence between concepts. To this end, we developed EL Box Embedding (ELBE) to learn Description Logic EL++embeddings using axis-parallel boxes. We generate specially designed box-based geometric constraints from EL++axioms for model training. Since the intersection of boxes remains as a box, the intersectional closure is satisfied. We report extensive experimental results on three datasets and present a case study to demonstrate the effectiveness of the proposed method.

Model checking is an automated technique for the verification of finite-state systems that is widely used in practice. In model checking, a model M is verified against a specification $\varphi$, exhaustively checking that the tree of all computations of M satisfies $\varphi$. When $\varphi$ fails to hold in M, the negative result is accompanied by a counterexample: a computation in M that demonstrates the failure. State of the art model checkers apply Binary Decision Diagrams(BDDs) as well as satisfiability solvers for this task. However, both methods suffer from the state explosion problem, which restricts the application of model checking to only modestly sized systems. The importance of model checking makes it worthwhile to explore alternative technologies, in the hope of broadening the applicability of the technique to a wider class of systems. Description Logic (DL) is a family of knowledge representation formalisms based on decidable fragments of first order logic. DL is used mainly for designing ontologies in information systems. In recent years several DL reasoners have been developed, demonstrating an impressive capability to cope with very large ontologies. This work consists of two parts. In the first we harness the growing ability of DL reasoners to solve model checking problems. We show how DL can serve as a natural setting for representing and solving a model checking problem, and present a variety of encodings that translate such problems into consistency queries in DL. Experimental results, using the Description Logic reasoner FaCT++, demonstrate that for some systems and properties, our method can outperform existing ones. In the second part we approach a different aspect of model checking. When a specification fails to hold in a model and a counterexample is presented to the user, the counterexample may itself be complex and difficult to understand. We propose an automatic technique to find the computation steps and their associated variable values, that are of particular importance in generating the counterexample. We use the notion of causality to formally define a set of causes for the failure of the specification on the given counterexample. We give a linear-time algorithm to detect the causes, and we demonstrate how these causes can be presented to the user as a visual explanation of the failure.

Model checking is an automated technique for the verification of finite-state systems that is widely used in practice. In model checking, a model M is verified against a specification $\varphi$, exhaustively checking that the tree of all computations of M satisfies $\varphi$. When $\varphi$ fails to hold in M, the negative result is accompanied by a counterexample: a computation in M that demonstrates the failure. State of the art model checkers apply Binary Decision Diagrams(BDDs) as well as satisfiability solvers for this task. However, both methods suffer from the state explosion problem, which restricts the application of model checking to only modestly sized systems. The importance of model checking makes it worthwhile to explore alternative technologies, in the hope of broadening the applicability of the technique to a wider class of systems. Description Logic (DL) is a family of knowledge representation formalisms based on decidable fragments of first order logic. DL is used mainly for designing ontologies in information systems. In recent years several DL reasoners have been developed, demonstrating an impressive capability to cope with very large ontologies. This work consists of two parts. In the first we harness the growing ability of DL reasoners to solve model checking problems. We show how DL can serve as a natural setting for representing and solving a model checking problem, and present a variety of encodings that translate such problems into consistency queries in DL. Experimental results, using the Description Logic reasoner FaCT++, demonstrate that for some systems and properties, our method can outperform existing ones. In the second part we approach a different aspect of model checking. When a specification fails to hold in a model and a counterexample is presented to the user, the counterexample may itself be complex and difficult to understand. We propose an automatic technique to find the computation steps and their associated variable values, that are of particular importance in generating the counterexample. We use the notion of causality to formally define a set of causes for the failure of the specification on the given counterexample. We give a linear-time algorithm to detect the causes, and we demonstrate how these causes can be presented to the user as a visual explanation of the failure.

Real-world automated reasoning systems, based on classical logic, face logically inconsistent information, and they must cope with it. It is onerous to develop such systems because classical logic is explosive. Recently, progress has been made towards semantics that deal with logical inconsistency. However, such semantics was never analyzed in the aspect of inconsistency tolerant relational model. In our research work, we use an inconsistency and incompleteness tolerant relational model called "Paraconsistent Relational Model." The paraconsistent relational model is an extension of the ordinary relational model that can store, not only positive information but also negative information. Therefore, a piece of information in the paraconsistent relational model has four truth values: true, false, both, and unknown. However, the paraconsistent relational model cannot represent disjunctive information (disjunctive tuples). We then introduce an extended paraconsistent relational model called disjunctive paraconsistent relational model. By using both the models, we handle inconsistency - similar to the notion of quasi-classic logic or four-valued logic -- in deductive databases (logic programs with no functional symbols). In addition to handling inconsistencies in extended databases, we also apply inconsistent tolerant reasoning technique in semantic web knowledge bases. Specifically, we handle inconsistency assosciated with closed predicates in semantic web. We use again the paraconsistent approach to handle inconsistency. We further extend the same idea to description logic programs (combination of semantic web and logic programs) and introduce dl-relation to represent inconsistency associated with description logic programs.

Extending Descriptions Logics (DLs) with a temporal dimension to aid in the ability to model meaningful temporal information is an active and popular research area that has gathered a lot of attention over recent years. DLs underpin the Web Ontology Language (OWL) which offers a way to describe ontologies for the semantic web. Representing temporal information in ontologies plays an important role, specifically for those ontologies where time information is inherently embedded in the information they describe. This is very common for ontologies in the bio-health domain, for example ontologies that describe the development of anatomies of biological entities, stage based development, evolution of diseases and so on. As expressive as DLs are, given that they are fragments of First Order Logic, they are static in nature and are limited in what they can express from a temporal view point, hence the surge in temporal extensions to DLs over recent years. In this thesis we investigate the use of temporal extensions of DLs as suitable representations for the temporal information required for bio-health ontologies. We first set out to find out exactly what types of temporal information need to be modelled, before going on to evaluate current temporal extensions and representations to determine their suitability. We then go on to introduce several new temporal extensions to DLs and evaluate their suitability.

Answering conjunctive queries over ontology-enriched datasets is a core reasoning task for many applications of semantic technologies. Conjunctive query answering is, however, computationally very expensive, which has led to the development of query answering procedures that sacrifice either the expressive power of ontology languages, or the completeness of query answers in order to improve scalability. This thesis describes a hybrid approach to query answering over OWL 2 ontologies that combines a datalog reasoner with a fully-fledged OWL 2 reasoner in order to provide scalable "pay-as-you-go" performance. The key feature of this hybrid approach is that it delegates the bulk of the computation to the datalog reasoner and resorts to expensive OWL 2 reasoning only as necessary to fully answer the query. Although the main goal of this thesis is to efficiently answer queries over OWL 2 ontologies, the technical results are more general and the approach is applicable to first-order knowledge representation languages that can be captured by rules allowing for existential quantification and disjunction in the head; the only assumption is the availability of a datalog reasoner and a fully-fledged reasoner for the language of interest, both of which are used as "black boxes". All techniques proposed in this thesis are implemented in the PAGOdA system, which combines the datalog reasoner RDFox and the OWL 2 reasoner HermiT. An extensive evaluation shows that PAGOdA succeeds in providing scalable pay-as-you-go query answering for a wide range of OWL 2 ontologies, datasets and queries.

Description Logics (DLs) form a family of languages which correspond to decidable fragments of First-Order Logic (FOL). They have been overwhelmingly successful for constructing ontologies - conceptual structures describing domain knowledge. Ontologies proved to be valuable in a range of areas, most notably, bioinformatics, chemistry, Health Care and Life Sciences, and the Semantic Web.One limitation of DLs, as fragments of FOL, is their restricted ability to cope with various forms of uncertainty. For example, medical knowledge often includes statistical relationships, e.g., findings or results of clinical trials. Currently it is maintained separately, e.g., in Bayesian networks or statistical models. This often hinders knowledge integration and reuse, leads to duplication and, consequently, inconsistencies.One answer to this issue is probabilistic logics which allow for smooth integration of classical, i.e., expressible in standard FOL or its sub-languages, and uncertain knowledge. However, probabilistic logics have long been considered impractical because of discouraging computational properties. Those are mostly due to the lack of simplifying assumptions, e.g., independence assumptions which are central to Bayesian networks.In this thesis we demonstrate that deductive reasoning in a particular probabilistic DL, called P-SROIQ, can be computationally practical. We present a range of novel algorithms, in particular, the probabilistic satisfiability procedure (PSAT) which is, to our knowledge, the first scalable PSAT algorithm for a non-propositional probabilistic logic. We perform an extensive performance and scalability evaluation on different synthetic and natural data sets to justify practicality.In addition, we study theoretical properties of P-SROIQ by formally translating it into a fragment of first-order logic of probability. That allows us to gain a better insight into certain important limitations of P-SROIQ. Finally, we investigate its applicability from the practical perspective, for instance, use it to extract all inconsistencies from a real rule-based medical expert system.We believe the thesis will be of interest to developers of probabilistic reasoners. Some of the algorithms, e.g., PSAT, could also be valuable to the Operations Research community since they are heavily based on mathematical programming. Finally, the theoretical analysis could be helpful for designers of future probabilistic logics.

Knowledge representation learning (KRL) has been a long-standing and challenging topic in artificial intelligence. Recent years have witnessed the rapidly growing research interest and industrial applications of KRL. However, two important aspects of KRL remains unsatisfactory in the academia and industries, i.e., the quality and the generalization capabilities of the learned representations. This thesis presents a set of methods target at learning high quality distributed knowledge representations and further empowering the learned representations for more general reasoning tasks over knowledge bases. On the one hand, we identify the false negative issue and the data sparsity issue in the knowledge graph completion (KGC) task that can limit the quality of the learned representations. Correspondingly, we design a ranking-based positive-unlabeled learning method along with an adversarial data augmentation strategy for KGC. Then we unify them seamlessly to improve the quality of the learned representations. On the other hand, although recent works expand the supported neural reasoning tasks remarkably by answering multi-hop logical queries, the generalization capabilities are still limited to inductive reasoning tasks that can only provide entity-level answers. In fact, abductive reasoning that provides concept-level answers to queries is also in great need by online users and a wide range of downstream tasks. Therefore, we design a joint abductive and inductive knowledge representation learning and reasoning system by incorporating, representing, and operating on concepts. Extensive experimental results along with case studies demonstrate the effectiveness of our methods in improving the quality and generalization capabilities of the learned distributed knowledge representations.

Virtual Enterprise (VE) is an organizational collaboration concept which provides a competitive edge in the globalized business environment. The life cycle of a VE consists of four stages i.e. opportunity identification (Pre-Creation), partner selection (Creation), operation and dissolution. The success of VEs depends upon the efficient execution of their VE-lifecycles along with knowledge enhancement for the partner enterprises to facilitate the future formation of efficient VEs. This research aims to study the different issues which occur in the VE lifecycle and provides a platform for the formation of high performance enterprises and VEs. In the pre-creation stage, enterprises look for suitable partners to create their VE and to exploit a market opportunity. This phase requires explicit and implicit information extraction from enterprise data bases (ECOS-ontology) for the identification of suitable partners. A description logic (DL) based query system is developed to extract explicit and implicit information and to identify potential partners for the creation of the VE. In the creation phase, the identified partners are analysed using different risks paradigms and a cooperative game theoretic approach is used to develop a revenue sharing mechanism based on enterprises inputs and risk minimization for optimal partner selection. In the operation phases, interoperability remains a key issue for seamless transfer of knowledge information and data. DL-based ontology mapping is applied in this research to provide interoperability in the VE between enterprises with different domains of expertise. In the dissolution stage, knowledge acquired in the VE lifecycle needs to be disseminated among the enterprises to enhance their competitiveness. A DL-based ontology merging approach is provided to accommodate new knowledge with existing data bases with logical consistency. Finally, the proposed methodologies are validated using the case study. The results obtained in the case study illustrate the applicability and effectiveness of proposed methodologies in each stage of the VE life cycle.

Access restrictions are essential in standard information systems and became an issue for ontologies in the following two aspects. Ontologies can represent explicit and implicit knowledge about an access policy. For this aspect we provided a methodology to represent and systematically complete role-based access control policies. Orthogonally, an ontology might be available for limited reading access. Independently of a specific ontology language or reasoner, we provided a lattice-based framework to assign labels to an ontology’s axioms and consequences. We looked at the problems to compute and repair one or multiple consequence labels and to assign a query-based access restriction. An empirical evaluation has shown that the algorithms perform well in practical scenarios with large-scale ontologies.