graph      ::= (triple)* 
triple     ::= subject predicate object 
subject    ::= iri | BlankNode | tripleTerm
predicate  ::= iri 
object     ::= iri | BlankNode | literal | tripleTerm
tripleTerm ::= triple
iri        ::= ... | rdf:reifies | ...

• RDF 1.1 syntax is the above without the tripleTerm category.
• A term is denoted by r, a triple by t, and a graph by g.
• Given a triple t, we denote the subject, predicate, object of t as t.s, t.p, t.o, respectively.

An RDF simple interpretation I is a structure <IR, IP, IS, IL, IEXT, RE> consisting of:

1. A non-empty set IR of resources, called the domain or universe of I.
2. A set IP, called the set of properties of I.
3. A mapping IS from IRIs into IR ⋃ IP, called the interpretation of IRIs.
4. A partial mapping IL from literal into IR, called the interpretation of literals.
5. A mapping IEXT from IP into 2IR x IR, called the extension of properties.
6. ⏩ A mapping RE from IR x IP x IR into IR, called the reification of triple terms. ⏪

A is a mapping from BlankNode to IR.

Given I and A, the function [I+A](.) is defined over terms, triples, and graphs as follows.

• [I+A](r) = IS(r)   if r is a iri
• [I+A](r) = IL(r)   if r is a literal
• ⏩ [I+A](r) = RE([I+A](r.s), [I+A](r.p), [I+A](r.o))   if r is a tripleTerm ⏪️
• [I+A](r) = A(r)   if r is a BlankNode

• [I+A](t) = TRUE   if and only if   <[I+A](t.s), [I+A](t.o)> ∈ IEXT([I+A](t.p))

• [I+A](g) = TRUE   if and only if   ∀ t ∈ g . [I+A](t) = TRUE

An interpretation I is a model of a graph g   if and only if   ∃ A . [I+A](g) = TRUE.

The set of all models of a graph g is called models(g).

Simple entailment: g ⊨ g'   if and only if   models(g) ⊆ models(g').

• RDF 1.1 semantics is the above without the parts within ⏩...⏪ marks, involving the tripleTerm category.

We introduce a macro for triple reification, which, as we will see, can be used to capture the use cases for reification, namely provenance, annotations, events, modalities, labelled property graph edges, n-ary relations, etc.

The syntax is extended as follows, in order to include the correct use of the macro.

(...)
subject           ::= iri | BlankNode | tripleTerm | tripleReification 
object            ::= iri | BlankNode | literal | tripleTerm | tripleReification 
tripleReification ::= identifier triple
reifier           ::= iri | BlankNode  
(...)

The macro for triple reification expands in the following way.

X1 X2 ( reifier triple ) . ➡️ reifier rdf:reifies triple . X1 X2 reifier .
( reifier triple ) X3 X4 . ➡️ reifier rdf:reifies triple . reifier X3 X4 .

A RDF graph which contains no triple terms nor rdf:reifies triples, with the exception of triple terms and rdf:reifies triples consistent with the expansion of occurrences of the macro for triple reification, is called reification well-formed. To be more precise, the explicit grammar for checking the reification well-formedness of RDF graphs is the following.

graph      ::= ( triple | reifier rdf:reifies tripleTerm )*
triple     ::= subject predicate object 
subject    ::= iri | BlankNode
predicate  ::= iri_but_rdf:reifies 
object     ::= iri | BlankNode | literal
tripleTerm ::= triple
reifier    ::= iri | BlankNode  

(...)