Recently, a lot of research has combined description logics (DLs) of the DL-Lite family with temporal formalisms. Such logics are proposed to be used for situation recognition and temporalized ontology-based data access. In this report, we consider DL-Lite-LTL, in which axioms formulated in a member of the DL-Lite family are combined using the operators of propositional linear-time temporal logic (LTL). We consider the satisfiability problem of this logic in the presence of so-called rigid symbols whose interpretation does not change over time. In contrast to more expressive temporalized DLs, the computational complexity of this problem is the same as for LTL, even w.r.t. rigid symbols.

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 complexity-wise than reasoning with unweighted automata. We also present explicit methods for solving these problems optimally.

Very recently, the tableau-based algorithm for deciding consistency of general fuzzy DL ontologies over the product t-norm was shown to be incorrect, due to a very weak blocking condition. In this report we take the first steps towards a correct algorithm by modifying the blocking condition, such that the (finite) structure obtained through the algorithm uniquely describes an infinite system of quadratic constraints. We show that this procedure terminates, and is sound and complete in the sense that the input is consistent iff the corresponding infinite system of constraints is satisfiable.

Ontology-based data access (OBDA) generalizes query answering in databases towards deduction since (i) the fact base is not assumed to contain complete knowledge (i.e., there is no closed world assumption), and (ii) the interpretation of the predicates occurring in the queries is constrained by axioms of an ontology. OBDA has been investigated in detail for the case where the ontology is expressed by an appropriate Description Logic (DL) and the queries are conjunctive queries. Motivated by situation awareness applications, we investigate an extension of OBDA to the temporal case. As query language we consider an extension of the well-known propositional temporal logic LTL where conjunctive queries can occur in place of propositional variables, and as ontology language we use the prototypical expressive DL ALC. For the resulting instance of temporalized OBDA, we investigate both data complexity and combined complexity of the query entailment problem.

[pt] Garantir que uma base de conhecimento com atos da administração pública contenha apenas fatos em conformidade com sua legislação torna-se um desafio para qualquer gestor público. Para isso, dado o grande volume de dados gerados por empresas públicas, faz-se necessário o emprego de recursos tecnológicos que auxiliem o processo de análise de conformidade destes atos. Este trabalho apresenta uma arquitetura computacional capaz de extrair informações publicados dos diários oficiais e então serializá-los em duas bases de conhecimento: triplas RDF/XML de fatos e triplas de RDF/XML de regras formalizadas em lógica iALC, uma lógica de descrição intuicionista. Para garantir a consistência desta base de conhecimento, foi desenvolvido um SAT Solver para iALC em forma de tableau semântico intuicionista. Uma extensão do tableau intuicionista de primeira ordem apresentado por Fitting (1969). Este SAT Solver faz parte de um módulo que além de gerar modelos e contra-exemplos para as regras formalizadas em iALC, também gera um código preliminar de consultas em SPARQL. Esta abordagem permite inferir e certificar a qualidade dos dados disponíveis na base de conhecimento RDF/XML de fatos. Para garantir a qualidade do nosso SAT Solver, fizemos a prova de soundness das suas regras. Para garantir a qualidade da nossa abordagem lógica, construímos um conjunto de 21 Questões de Competência e aplicamos à nossa ferramenta. Os resultados deste estudo de caso mostraram a eficácia e eficiência da nossa abordagem. / [en] Ensuring that a knowledge base with public administration acts contains only facts in accordance with its legislation becomes a challenge for any public manager. To achieve this, given the large volume of data generated by public companies, it is necessary to apply technological resources that assist in the process of analyzing the compliance of these acts. This work presents a computational architecture capable of extracting information published in official gazettes and then serializing it into two knowledge bases, RDF/XML triples of facts and RDF/XML triples of rules formalized in iALC logic, an intuitionistic description logic. To ensure the consistency of this knowledge base, a SAT Solver for iALC was developed in the form of an intuitionistic semantic tableau. An extension of the first-order intuitionist tableau presented by Fitting (1960). This SAT Solver is part of a module that generates models and counter-examples for rules formalized in iALC and generates a preliminary query code in SPARQL. This approach allows infer and certify the quality of the data available in the RDF/XML knowledge base of facts. To guarantee the quality of our SAT Solver, we carry out the soundness proof of its rules. To ensure the quality of our logical approach, we built a set of 21 Competency Questions and applied our tool. The results of this case study showed our approach s effectiveness and efficiency.

We propose an interactive repair method for the description logic EL that is based on the optimal-repair framework. The obtained repair might not be optimal in the theoretical sense, i.e. more than a minimal amount of consequences might have been removed---but from a practical perspective it is superior to a theoretically optimal repair as the interaction strategy enables the users to identify further faulty consequences connected to the initially reported errors. / This is an extended version of an article accepted at the KRR track of the 40th ACM/SIGAPP Symposium On Applied Computing (SAC 2025).

In applications of AI systems where exact definitions of the important notions of the application domain are hard to come by, the use of traditional logic-based knowledge representation languages such as Description Logics may lead to very large and unintuitive definitions, and high complexity of reasoning. To overcome this problem, we define new concept constructors that allow us to define concepts in an approximate way. [... from the abstract]

We present an FCA-based axiomatization method that produces a complete EL TBox (the terminological part of an OWL 2 EL ontology) from a graph dataset in at most exponential time. We describe technical details that allow for efficient implementation as well as variations that dispense with the computation of extremely large axioms, thereby rendering the approach applicable albeit some completeness is lost. Moreover, we evaluate the prototype on real-world datasets. / This is an extended version of an article accepted at AAAI 2024.

Ontology-mediated query answering is a popular paradigm for enriching answers to user queries with background knowledge. For querying the absence of information, however, there exist only few ontology-based approaches. Moreover, these proposals conflate the closed-domain and closed-world assumption, and therefore are not suited to deal with the anonymous objects that are common in ontological reasoning. We propose a new closed-world semantics for answering conjunctive queries with negation over ontologies formulated in the description logic ELH⊥, which is based on the minimal canonical model. We propose a rewriting strategy for dealing with negated query atoms, which shows that query answering is possible in polynomial time in data complexity.

Lightweight temporal ontology languages have become a very active field of research in recent years. Many real-world applications, like processing electronic health records (EHRs), inherently contain a temporal dimension, and require efficient reasoning algorithms. Moreover, since medical data is not recorded on a regular basis, reasoners must deal with sparse data with potentially large temporal gaps. In this paper, we introduce a temporal extension of the tractable language ELH⊥, which features a new class of convex diamond operators that can be used to bridge temporal gaps. We develop a completion algorithm for our logic, which shows that entailment remains tractable. Based on this, we develop a minimal-world semantics for answering metric temporal conjunctive queries with negation. We show that query answering is combined first-order rewritable, and hence in polynomial time in data complexity.