We propose a new integration of rule reasoners with one or more RDF stores, using selective SPARQL queries to fetch relevant data. In contrast to previous implementations that merely import results of fixed SPARQL queries, our approach relies on pure logic programs over RDF triple data. Transparent to the user, optimised SPARQL queries then are constructed and evaluated during reasoning. To ensure good performance, we develop optimisation methods that adopt ideas from logic program optimisation, including semi-naive evaluation, magic sets, and static filtering. Based on the integration of our methods into the open source rule engine Nemo, we empirically evaluate our approach with complex rule sets over large knowledge graphs.

Static filtering is a data-independent optimisation method for Datalog, which generalises algebraic query rewriting techniques from relational databases. In spite of its early discovery by Kifer and Lozinskii in 1986, the method has been overlooked in recent research and system development, and special cases are being rediscovered independently. We therefore recall the original approach, using updated terminology and more general filter predicates that capture features of modern systems, and we show how to extend its applicability to answer set programming (ASP). The outcome is strictly more general but also more complex than the classical approach: double exponential in general and single exponential even for predicates of bounded arity. As a solution, we propose tractable approximations of the algorithm that can still yield much improved logic programs in typical cases, e.g., it can improve the performance of rule systems over real-world data in the order of magnitude.

Combining RDF rule languages, such as N3 or SHACL Rules, with default negation is challenging. Existing methods to stratify negation often fail for RDF rules, since individual triples do not carry enough information to meaningfully restrict potential dependencies. Blank nodes in rule heads further complicate the matter, since the order of rule applications may determine whether new values are created, which in turn can change the applicability of rules with negation. To solve these open problems, we propose chain stratification as a robust new condition that guarantees a well-behaved semantics for RDF rules with negation, and existential rules in general. Our condition combines an elaborate analysis of potential multistep derivations with a mechanism for using integrity constraints to discard impossible cases. Applying rules in any order that respects chain stratification is guaranteed to derive an RDF graph that is unique, lean, and justified under the usual negation-as-failure semantics. To show the practicality, we also provide a prototype implementation.

Datalog rules are often used to define ontologies over Knowledge Graphs. Rule reasoners routinely optimise such ontologies by rewriting their rules into a form that can be evaluated more efficiently. These transformations preserve the entailed facts, but not the structure of the underlying derivations. A proof tree under the rewritten rules explains why a fact holds, but does not readily yield an explanation in terms of the original rules. We study the problem of constructing, from a proof of entailment under the rewritten rules, a proof under the original ones: we establish its computational complexity and identify two practically relevant languages for specifying proof transformations.

Nemo Explain Visualizer (nev) is an interactive visual query tracer and builder for Nemo, a powerful Datalog reasoner with extended features. Our tools were developed with and for expert users. However, considering the lack of resources to learn Datalog and similar declarative logic programming languages, we conducted a qualitative user study to assess how our tools might help students. The study, interviewing 14 participants with varying levels of involvement with the content of a university course on knowledge graphs, revealed a very positive assessment of our tools, which strengthens the value of visual explanation tools beyond their intended use.

Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and, in principle, explainable by design, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.

Consequence-based reasoning can be used to construct proofs that explain entailments of description logic (DL) ontologies. In the literature, one can find multiple consequence-based calculi for reasoning in the ℰℒ family of DLs, each of which gives rise to proofs of different shapes. Here, we study three such calculi and the proofs they produce on a benchmark based on the OWL Reasoner Evaluation. The calculi are implemented using a translation into existential rules with stratified negation, which had already been demonstrated to be effective for the calculus of the ELK reasoner. We then use the rule engine NEMO to evaluate the rules and obtain traces of the rule execution. After translating these traces back into DL proofs, we compare them on several metrics that reflect different aspects of their complexity.

We propose the RISKMAN ontology and shapes for representing and analysing information about risk management for medical devices. Risk management is concerned with taking necessary precautions to ensure that a medical device does not cause harms for users or the environment. To date, risk management documentation is submitted to notified bodies (for certification) in the form of semi-structured natural language text. We propose to use terms from the RISKMAN ontology to provide a formal, logical underpinning for risk management documentation, and to use the included SHACL constraints to check whether the provided data is in accordance with the requirements of the two relevant norms, i.e. ISO 14971 and VDE Spec 90025. RISKMAN is available at https://w3id.org/riskman.

The chase is a widely implemented approach to reason with tuple-generating dependencies (tgds), used in data exchange, data integration, and ontology-based query answering. However, it is merely a semi-decision procedure, which may fail to terminate. Many decidable conditions have been proposed for tgds to ensure chase termination, typically by forbidding some kind of "cycle" in the chase process. We propose a new criterion that explicitly allows some such cycles, and yet ensures termination of the standard chase under reasonable conditions. This leads to new decidable fragments of tgds that are not only syntactically more general but also strictly more expressive than the fragments defined by prior acyclicity conditions. Indeed, while known terminating fragments are restricted to PTime data complexity, our conditions yield decidable languages for any k-ExpTime. We further refine our syntactic conditions to obtain fragments of tgds for which an optimised chase procedure decides query entailment in PSpace or k-ExpSpace, respectively.

We present Nemo, a toolkit for rule-based reasoning and data processing that emphasises robustness and ease of use. Nemo’s core is a scalable and efficient main-memory reasoner that supports an expressive extension of Datalog with support for datatypes, existential rules, aggregates, and (stratified) negation. Built around this core is a versatile system of libraries and applications for interfacing with several data formats and programming languages, use as a progressive web application, and IDE integration. In this system description, we present this toolkit and discuss relevant application areas in rule-based knowledge representation, knowledge graph processing, and reasoner prototyping. Our evaluation on a range of tasks from these areas demonstrates Nemo’s robust performance in comparison to state-of-the-art rule engines.

We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.

This short paper reviews the main contributions of our recent work on static analysis of existential rules (a.k.a. tuple-generating dependencies). Between such rules, several kinds of logical relationships – also called dependencies in an unfortunate clash of terminology – are of interest, but their computation highly intractable ( Σ P2 -complete). We develop new, optimised procedures for this task, and present a prototype implementation that scales to rule sets with more than 100,000 rules. This allows us to perform much faster acyclicity checks and to identify rule sets that admit e ffi cient core computation via the standard chase.

Wikidata, now a decade old, is the largest public knowledge graph, with data on more than 100 million concepts contributed by over 560,000 editors. It is widely used in applications and research. At its launch in late 2012, however, it was little more than a hopeful new Wikimedia project, with no content, almost no community, and a severely restricted platform. Seven years earlier still, in 2005, it was merely a rough idea of a few PhD students, a conceptual nucleus that had yet to pick up many important influences from others to turn into what is now called Wikidata. In this paper, we try to recount this remarkable journey, and we review what has been accomplished, what has been given up on, and what is yet left to do for the future.

This repository contains the input data for the evaluation presented in the following publication: David Carral, Irina Dragoste, Markus Krötzsch: The Combined Approach to Query Answering in Horn-ALCHOIQ. Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018). Together with the materials in https://github.com/knowsys/eval-combined-approach-horn-alchoiq, the input data here provides all the necessary tools and datasets to reproduce the experiments described in this paper.Contents:- input_files_for_Konclude - input data for the experiments that use Konclude tool- input_files_for_RDFox - input data for the experiments that use our prototype (https://github.com/knowsys/eval-combined-approach-horn-alchoiq/tree/master/combined-approach), which is based on RDFox tool- RDFox_dependency - the RDFox reasoner version used in our prototype implementation

This system demonstration presents Nemo, a new logic programming engine with a focus on reliability and performance. Nemo is built for data-centric analytic computations, modelled in a fully declarative Datalog dialect. Its scalability for these tasks matches or exceeds that of leading Datalog systems. We demonstrate uses in reasoning with knowledge graphs and ontologies with 10^5 to 10^8 input facts, all on a laptop. Nemo is written in Rust and available as a free and open source tool.