Weighted automata can be seen as a natural generalization of finite state automata to more complex algebraic structures. The standard reasoning tasks for unweighted automata can also be generalized to the weighted setting. In this report we study the problems of intersection, complementation and inclusion for weighted automata on infinite trees and show that they are not harder than reasoning with unweighted automata. We also present explicit methods for solving these problems optimally.

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. The inexpressive Description Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has recently been shown to be NP-complete, and thus of significantly lower complexity than unification in other DLs of similarly restricted expressive power. However, the unification algorithms for EL developed so far cannot deal with general concept inclusion axioms (GCIs). This paper makes a considerable step towards addressing this problem, but the GCIs our new unification algorithm can deal with still need to satisfy a certain cycle restriction.

Fuzzy description logics (DLs) have been investigated for over two decades, due to their capacity to formalize and reason with imprecise concepts. Very recently, it has been shown that for several fuzzy DLs, reasoning becomes undecidable. Although the proofs of these results differ in the details of each specific logic considered, they are all based on the same basic idea. In this report, we formalize this idea and provide sufficient conditions for proving undecidability of a fuzzy DL. We demonstrate the effectiveness of our approach by strengthening all previously-known undecidability results and providing new ones. In particular, we show that undecidability may arise even if only crisp axioms are considered.

We extend previous results on the complexity of solving language equations with one-sided concatenation and all Boolean operations to the case where also disequations (i.e., negated equations) may occur. To show that solvability of systems of equations and disequations is still in ExpTime, we introduce a new type of automata working on infinite trees, which we call looping automata with colors. As applications of these results, we show new complexity results for disunification in the description logic FL₀ and for monadic set constraints with negation. We believe that looping automata with colors may also turn out to be useful in other applications. / A short version of this report has also appeared in Proceedings of LPAR-18, Springer LNCS 7180, 2012.

Unification in Description Logics has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the Description Logic EL, which is used to define several large biomedical ontologies, unification is NP-complete. An NP unification algorithm for EL based on a translation into propositional satisfiability (SAT) has recently been presented. In this report, we extend this SAT encoding in two directions: on the one hand, we add general concept inclusion axioms, and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the translation to be complete, however, the ontology needs to satisfy a certain cycle restriction. The SAT translation depends on a new rewriting-based characterization of subsumption w.r.t. ELHR+-ontologies.

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL EL, which is used to define several large biomedical ontologies, unification is NP-complete. A goal-oriented NP unification algorithm for EL that uses nondeterministic rules to transform a given unification problem into solved form has recently been presented. In this report, we extend this goal-oriented algorithm in two directions: on the one hand, we add general concept inclusion axioms (GCIs), and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the algorithm to be complete, however, the ontology consisting of the GCIs and role axioms needs to satisfy a certain cycle restriction.

Unification has been introduced in Description Logic (DL) as a means to detect redundancies in ontologies. In particular, it was shown that testing unifiability in the DL EL is an NP-complete problem, and this result has been extended in several directions. Surprisingly, it turned out that the complexity increases to PSpace if one disallows the use of the top concept in concept descriptions. Motivated by features of the medical ontology SNOMED CT, we extend this result to a setting where the top concept is disallowed, but there is a background ontology consisting of restricted forms of concept and role inclusion axioms. We are able to show that the presence of such axioms does not increase the complexity of unification without top, i.e., testing for unifiability remains a PSpace-complete problem.

We introduce an extension of the Description Logic FL0 that allows us to define concepts in an approximate way. More precisely, we extend FL0 with a threshold concept constructor of the form Ct><l t for t><l ∈ {≤, <, ≥, >}, whose semantics is given by using a membership distance function (mdf). A membership distance function m assigns to each domain element and concept a distance value expressing how “close” is such element to being an instance of the concept. Based on this, a threshold concept Ct><l t is interpreted as the set of all domain elements that have a distance s from C such that s t><l t. We provide a framework to obtain membership distance functions based on functions that compare tuples of languages, and we show how weighted looping tree automata over a semiring can be used to define membership distance functions for FL0 concepts. / This is an extended version of an article accepted at the 36th International Workshop on Description Logics (DL 2023).

Formal ontologies are of significant importance in artificial intelligence, playing a central role in the Semantic Web, ontology-based information integration, or peer-to-peer data management. In such scenarios, an especially prominent role is played by description logics (DLs) – a robust family of logical formalisms used to describe ontologies and serving as the logical underpinning of contemporary standardised ontology languages. To put knowledge bases to full use as core part of intelligent information systems, much attention is being devoted to the area of ontology-based data-access, with conjunctive queries and their generalisations such as positive conjunctive two-way regular path queries being employed as a fundamental querying formalism. The most expressive exemplars of description logics feature advanced constructors for roles and path expressions. Among the most powerful knowledge representation formalisms on the verge of decidability, are the DLs from the Z family. For its most expressive proponent, ZOIQ (a.k.a. ALCHbSelf reg OIQ), featuring nominals (O), role inverses (I), and number restrictions (Q), querying is undecidable and even decidability of knowledge-base satisfiability is open, owing to the intricate interplay of the three mentioned features. Restricting the interaction of O, I, and Q however (or excluding one of the features altogether) leads to beneficial model-theoretic properties, which give rise to upper bounds of ExpTime for knowledge-base satisfiability and 2ExpTime for querying. Aiming for better understanding of the “expressive power versus computational complexity” trade-off for the Z family of DLs, we provide a more fine-grained complexity analysis for the query entailment problem over ontologies. In the thesis we focus on tame fragments of ZOIQ, namely the fragments in which either one the three features from {I, O, Q} is dropped or the class of models is restricted to the so-called quasi-forests. We employ the query languages ranging from (unions of) conjunctive queries ((U)CQs) to positive two-way regular path queries (P2RPQs). We mostly follow the classical semantics of entailment, but we also provide several results in the “finite-model” scenario. The most important results of the thesis are summarised below. 1. We provide a complete classification of the complexity of the query entailment problem (for various query languages discussed above) for tamed fragments of ZOIQ under the classical semantics. This involves several new ingredients such as: (i) a uniform exponential-time algorithm based on Lutz’s spoiler technique for the entailment of unions of conjunctive queries for ALCHbreg, (ii) new lower bounds for (rooted and unrooted) conjunctive query entailment over ALCSelf ontologies, and (iii) a novel reduction from the entailment of P2RPQs to the satisfiability problem for tamed ZOIQ, yielding a uniform 2ExpTime upper bound for all the considered logics. As a preliminary step towards lifting the above results to the realm of data complexity, we establish that the satisfiability of tamed ZOIQ is NP-complete. 2. Under the finite model semantics, we focus on UCQs only. With the proviso that the finite satisfiability problem for ZIQ is ExpTime-complete, we also provide a complete picture of the complexity of the query entailment problems. The key insight is that ZOI and ZOQ are finitely controllable. 3. We conclude the thesis by investigating the decidability border of further extensions of the Z family of DLs. Our goal is to understand whether the class of regular languages present in path expressions in Z is maximal for guaranteeing decidability of the underlying logic. We provide a series of undecidability results involving simple, non-regular languages (a subclass of visibly pushdown languages). Our proofs rely on well-established model- and graph-theoretic definitions. What is more, most of them generalise (in a uniform way) and solidify multiple results known by the DL community. Our proofs are also easily adjustable to freshly defined logics, without the need to reproduce nearly-identical proofs.

Submitted by Luciana Ferreira (lucgeral@gmail.com) on 2018-02-23T12:55:26Z No. of bitstreams: 2 Dissertação - Luiz Gustavo Dias - 2018.pdf: 24658970 bytes, checksum: e3353986b772fe9103c6a705f3aa4ee0 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2018-02-23T12:56:11Z (GMT) No. of bitstreams: 2 Dissertação - Luiz Gustavo Dias - 2018.pdf: 24658970 bytes, checksum: e3353986b772fe9103c6a705f3aa4ee0 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-02-23T12:56:11Z (GMT). No. of bitstreams: 2 Dissertação - Luiz Gustavo Dias - 2018.pdf: 24658970 bytes, checksum: e3353986b772fe9103c6a705f3aa4ee0 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2018-01-30 / Nowadays to manage knowledge from corporate activities, competency management is increasingly effective in the process of defining organizational strategies. In this way, the present research had the purpose to use formal methods to verify if functions from positions, and competences coming from employees that occupy them, can interfere in the functioning of organizations. A long this lines, an ontology was developed using methodology 101, which had as its domain the educational sector, and served as an information base for the execution of queries elaborated from the description logic, in order to find possible inconsistencies as well as solutions. During the study of the case, were found inconsistencies related to qualification, training, stocking and compatibility of information from different sources that represented the same domain. As a result the research allowed the creation of correct knowledge and that can be used by managers, at different hierarchical levels, helping in the improvement of processes and decision making. / Com a necessidade de gerenciar o conhecimento advindo das atividades corporativas, a gerência de competências se mostra cada vez mais efetiva no processo de definição de estratégias Organizacionais. Desta forma a presente pesquisa objetivou utilizar métodos formais para verificar se funções advindas de cargos, e competências advindas de colaboradores que ocupam os mesmos, podem interferir no funcionamento de organizações. Tendo em vista essa necessidade, foi produzida nesta pesquisa uma ontologia utilizando a metodologia 101, que teve como domínio o setor educacional, e serviu de base de informações para a execução de consultas elaboradas a partir da lógica de descrição, a fim de encontrar possíveis inconsistências bem como soluções. Durante a realização do estudo de caso, foram encontradas inconsistências relacionadas a qualificação, capacitação, lotação e compatibilidade de informações advindas de fontes diferentes que representavam o mesmo domínio. Como resultado a pesquisa possibilitou a criação de conhecimento correto e que pode ser empregado por gestores, em diferentes níveis hierárquicos, auxiliando na melhoria de processos e tomadas de decisões.