Notation3: Graph Terms for RDF

Dörthe Arndt; Pierre-Antoine Champin

Home/Archive/arXiv

arXiv · 2610.31266

Notation3: Graph Terms for RDF

Dörthe Arndt·Pierre-Antoine Champin

View original source ↗Read source document ↗Export metadata ↓

Abstract

Notation3 Logic was introduced as an extension of RDF allowing the user to express rules on top of triples and to make statements about graphs. The original proposal of the logic only came with an informal specification of its semantics which has been refined later on. While this refinement clarified the meaning of rules and implicitly quantified variables, it left the meaning of graphs used as terms - so-called graph terms - open. In this paper we aim to close this gap. We discuss in detail, how graph terms are used in Notation3, which formal requirements they need to meet, and provide examples to illustrate the difficulties when defining their semantics. We then introduce an abstract syntax for the logic and define its semantics in two steps: similarly to RDF's simple interpretations, we define interpretations and basic entailment for Notation3 which covers plain RDF triples but also triples containing graph terms. N3-entailment is then an extension of basic entailment which assigns meaning to the different special predicates of the logic like for example the implication symbol. N3-entailment is defined in a way that it can be extended whenever a new predicate is added to the logic. As Notation3 Logic is currently under development, we expect many predicates to be added. Our research provides and important step towards the full standardisation of the logic.

Explore related subjects

cs.LO cs.AI

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Dörthe Arndt, Pierre-Antoine Champin. 2026-10-22. Notation3: Graph Terms for RDF. https://arxiv.org/abs/2610.31266

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A declarative approach to specifying Paxos using three-valued modal fixpoint logic

We present Three-valued Fixpoint Quorum Logic, or 3muQL for short; a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm. Our methodology represents a distributed algorithm as a logical theory, enabling correctness properties to be derived directly within the framework -- or revealing logical errors in the algorithm's design when they exist. 3muQL adopts a declarative approach, specifying the overall logic of computation without prescribing control flow. Notably, message-passing and state-transitions are not explicitly modelled, and notions of 'quorum' are abstracted from concrete thresholds to abstract modal operators. This distinguishes our framework from approaches like TLA+. The logical abstraction emphasises the essence of distributed algorithms, offering a novel perspective on their specification and reasoning. We define the syntax and semantics of 3muQL, explore its theoretical properties, and demonstrate its applicability through a detailed treatment of the Paxos consensus algorithm. By presenting Paxos as a logical theory and deriving its standard correctness properties, we showcase the framework's capacity to handle non-trivial distributed systems. We envision 3muQL as a versatile tool for specifying and reasoning about distributed algorithms. The Paxos example highlights the framework's ability to capture intricate details, offering a new lens through which distributed algorithms can be specified, studied, and checked. The ideas we present are easily implemented, and to demonstrate this we have implemented a freely-available proof-of- concept 3muQL model-checker, as an effective prototyping tool.

cs.LO↗

arXiv2026

Ohana trees, linear approximation and multi-types for the $λ$I-calculus: No variable gets left behind or forgotten!

Although the $λ$I-calculus is a natural fragment of the $λ$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable $λ$I-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the $λ$I-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a $λ$I-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach -- more classic -- is based on finite trees and continuity, the second adapts Ehrhard and Regnier's Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a $λ$I-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. Subsequently, we introduce a denotational model designed to capture the equality induced by Ohana trees. Although presented as a non-idempotent type system, our model is based on a suitably modified version of the relational semantics of the $λ$-calculus, which is known to yield proper models of the $λ$I-calculus when restricted to non-empty finite multisets. To track variables occurring in subterms that are hidden or pushed to infinity in the evaluation trees, we generalize the system in two ways: first, we reintroduce annotated versions of the empty multiset indexed by sets of variables; second, (...)

cs.LO↗

arXiv2026

A simple formalization of alpha-equivalence

While teaching untyped $λ$-calculus to undergraduate students, we were wondering why $α$-equivalence is not directly inductively defined. In this paper, we demonstrate that this is indeed feasible. Specifically, we provide a grounded, inductive definition for $α$-equivalence and show that it conforms to the specification provided in the literature. The work presented in this paper is fully formalized in the Rocq Prover.

cs.LO↗