Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Existential Notation3 Logic

Dörthe Arndt, Stephan Mennicke

TL;DR

The paper tackles the challenge of fast reasoning with Notation3 Logic by isolating an existential fragment ${N3}^exists$ that corresponds to existential rules. It defines the syntax and semantics, establishes a piece-normal-form (PNF) representation, and builds a translation ${\mathcal{T}}$ from ${N3}^exists$ to existential rules, proving that the translation preserves equivalence. The authors implement this translation and empirically compare N3 reasoners (EYE, cwm) with existential-rule engines (VLog, Nemo) on Lubm and Deep Taxonomy datasets, finding that existential-rule reasoners excel with large data, while EYE excels with very dependent rule sets. The work demonstrates practical potential for cross-pollination between Semantic Web rule formats and database-style existential rules, and it lays groundwork for extending the approach to N3 lists and built-ins. Overall, the results suggest that translating N3 reasoning to existential-rule frameworks can broaden tool support and improve performance for data-intensive Web reasoning tasks.

Abstract

In this paper, we delve into Notation3 Logic (N3), an extension of RDF, which empowers users to craft rules introducing fresh blank nodes to RDF graphs. This capability is pivotal in various applications such as ontology mapping, given the ubiquitous presence of blank nodes directly or in auxiliary constructs across the Web. However, the availability of fast N3 reasoners fully supporting blank node introduction remains limited. Conversely, engines like VLog or Nemo, though not explicitly designed for Semantic Web rule formats, cater to analogous constructs, namely existential rules. We investigate the correlation between N3 rules featuring blank nodes in their heads and existential rules. We pinpoint a subset of N3 that seamlessly translates to existential rules and establish a mapping preserving the equivalence of N3 formulae. To showcase the potential benefits of this translation in N3 reasoning, we implement this mapping and compare the performance of N3 reasoners like EYE and cwm against VLog and Nemo, both on native N3 rules and their translated counterparts. Our findings reveal that existential rule reasoners excel in scenarios with abundant facts, while the EYE reasoner demonstrates exceptional speed in managing a high volume of dependent rules. Additionally to the original conference version of this paper, we include all proofs of the theorems and introduce a new section dedicated to N3 lists featuring built-in functions and how they are implemented in existential rules. Adding lists to our translation/framework gives interesting insights on related design decisions influencing the standardization of N3.

Existential Notation3 Logic

TL;DR

The paper tackles the challenge of fast reasoning with Notation3 Logic by isolating an existential fragment that corresponds to existential rules. It defines the syntax and semantics, establishes a piece-normal-form (PNF) representation, and builds a translation from to existential rules, proving that the translation preserves equivalence. The authors implement this translation and empirically compare N3 reasoners (EYE, cwm) with existential-rule engines (VLog, Nemo) on Lubm and Deep Taxonomy datasets, finding that existential-rule reasoners excel with large data, while EYE excels with very dependent rule sets. The work demonstrates practical potential for cross-pollination between Semantic Web rule formats and database-style existential rules, and it lays groundwork for extending the approach to N3 lists and built-ins. Overall, the results suggest that translating N3 reasoning to existential-rule frameworks can broaden tool support and improve performance for data-intensive Web reasoning tasks.

Abstract

In this paper, we delve into Notation3 Logic (N3), an extension of RDF, which empowers users to craft rules introducing fresh blank nodes to RDF graphs. This capability is pivotal in various applications such as ontology mapping, given the ubiquitous presence of blank nodes directly or in auxiliary constructs across the Web. However, the availability of fast N3 reasoners fully supporting blank node introduction remains limited. Conversely, engines like VLog or Nemo, though not explicitly designed for Semantic Web rule formats, cater to analogous constructs, namely existential rules. We investigate the correlation between N3 rules featuring blank nodes in their heads and existential rules. We pinpoint a subset of N3 that seamlessly translates to existential rules and establish a mapping preserving the equivalence of N3 formulae. To showcase the potential benefits of this translation in N3 reasoning, we implement this mapping and compare the performance of N3 reasoners like EYE and cwm against VLog and Nemo, both on native N3 rules and their translated counterparts. Our findings reveal that existential rule reasoners excel in scenarios with abundant facts, while the EYE reasoner demonstrates exceptional speed in managing a high volume of dependent rules. Additionally to the original conference version of this paper, we include all proofs of the theorems and introduce a new section dedicated to N3 lists featuring built-in functions and how they are implemented in existential rules. Adding lists to our translation/framework gives interesting insights on related design decisions influencing the standardization of N3.
Paper Structure (25 sections, 8 theorems, 67 equations, 2 figures, 1 table)

This paper contains 25 sections, 8 theorems, 67 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Motivation
  3. Existential N3
  4. Syntax
  5. Semantics
  6. Piece Normal Form
  7. From N3 to Existential Rules
  8. Foundations of Existential Rule Reasoning
  9. The Translation Function from N3 to Existential Rules
  10. Translating Atomic Pieces.
  11. Translating Rules.
  12. Translating the PNF.
  13. Correctness of the Translation
  14. Reasoning with Lists
  15. N 3 Lists
  16. ...and 10 more sections

Key Result

Lemma 1

Let $f=f_1f_2$ be an ${N\oldstylenums 3}\xspace^\exists$ conjunction and let $\operatorname{comp}(f_1)\cap\operatorname{comp}(f_2)\cap E=\emptyset$, then for each interpretation $\mathfrak{I}$, $\mathfrak{I}\models f \text{ iff } \mathfrak{I}\models f_1 \text{ and } \mathfrak{I}\models f_2$.

Figures (2)

  • Figure 1: Syntax of $\operatorname{N3}^\exists$
  • Figure 2: Structure of the Deep Taxonomy benchmark.

Theorems & Definitions (17)

  • Lemma 1: Pieces
  • proof
  • Lemma 2: Eliminating Existentials
  • proof
  • Definition 3: Piece Normal Form
  • Theorem 4
  • proof
  • Lemma 5
  • proof
  • Theorem 6
  • ...and 7 more