Reasoning with N3 · Chapter 2 of 10

Chapter 2

N3 in fifteen minutes

Notation3 is Turtle with two additions: graphs you can quote, and rules that turn one quoted graph into another. This chapter covers enough of it to read and write every rule in this book.

Facts

A fact is a triple: subject, predicate, object, then a full stop. Names are IRIs, usually shortened with a prefix. a is short for rdf:type. A semicolon repeats the subject, a comma repeats subject and predicate.

@prefix v: <urn:tiramemsu:v:>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.

v:socrates a v:Human.
v:alice v:worksAt v:acme;
    v:name "Alice";
    v:age 34.
v:acme v:locatedIn v:berlin, v:europe.
v:e1 v:validFrom "2020-01-01T00:00:00Z"^^xsd:dateTime.

Literals are strings, numbers, booleans, or typed values such as "2020-01-01T00:00:00Z"^^xsd:dateTime. Every prefix used must be declared with @prefix. The examples in this book always declare them, so every block is a complete N3 document you can paste into a file.

The prefixes you will see:

Formulas

Curly braces quote a graph. { v:socrates a v:Human } is a single term that stands for that graph. It does not assert the triple inside. A formula can be the subject or object of a triple, which is how N3 talks about statements:

@prefix v: <urn:tiramemsu:v:>.

v:plato v:said { v:socrates a v:Human }.

This says Plato said something. It does not say Socrates is human. Formulas are how rules are written, and, in chapter 3, how tiramemsu shows a rule what a statement says.

Rules

A rule is a triple whose subject and object are formulas and whose predicate is =>, read “implies”. The left formula is the body, the right one the head.

socrates.n3

@prefix v: <urn:tiramemsu:v:>.

v:socrates a v:Human.
{ ?x a v:Human } => { ?x a v:Mortal }.

Names that start with ? are variables. A variable is universally quantified over its rule: for every ?x that makes the body true, the head is true. A body with several triples is a conjunction. All of them must match, with the same value for the same variable.

A reasoner applies the rules to the facts, adds what they conclude, and repeats until nothing new appears. This is forward chaining. Rules feed each other:

@prefix v: <urn:tiramemsu:v:>.

{ ?x a v:Human } => { ?x a v:Mortal }.
{ ?x a v:Mortal } => { ?x v:has v:lifespan }.

From v:socrates a v:Human the reasoner concludes v:socrates a v:Mortal, then v:socrates v:has v:lifespan. The second conclusion rests on the first. Tiramemsu keeps that chain when it writes them (chapter 7).

Inventing a node

A blank node in a head, written _:name, means “there exists something”. Each time the rule fires, the reasoner invents a node for it:

@prefix v: <urn:tiramemsu:v:>.

{ ?x a v:Employee } => { ?x v:manager _:m. _:m a v:Manager }.

Bob is an employee, so Bob has some manager, and that manager is a manager. Nobody knows who. An invented node is called a Skolem node. Writing one to memory needs care, because running the rule twice must not invent two managers. Chapter 7 shows how tiramemsu keeps it stable.

Builtins

Some predicates compute instead of match. They are called builtins, and their prefixes say what they work on. A builtin in a body succeeds or fails like any other triple, and may bind variables.

builtins.n3

@prefix v: <urn:tiramemsu:v:>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix string: <http://www.w3.org/2000/10/swap/string#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

# Comparison: adults are at least 18.
{ ?p v:age ?a. ?a math:greaterThan 17 } => { ?p a v:Adult }.

# Arithmetic: the subject is a list of inputs, the object the result.
{ ?o v:net ?n; v:tax ?t. (?n ?t) math:sum ?g } => { ?o v:gross ?g }.

# Strings.
{ ?p v:first ?f; v:last ?l. (?f " " ?l) string:concatenation ?full } => { ?p v:fullName ?full }.
{ ?p v:title ?t. ?t string:startsWith "Dr" } => { ?p a v:Doctor }.

# Term equality.
{ ?a v:worksAt ?c. ?b v:worksAt ?c. ?a log:notEqualTo ?b } => { ?a v:sharesEmployerWith ?b }.

Some builtins look at more than one fact at a time. They need extra care in a memory, because adding a fact can make their answer false:

careful.n3

@prefix v: <urn:tiramemsu:v:>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix list: <http://www.w3.org/2000/10/swap/list#>.
@prefix time: <http://www.w3.org/2000/10/swap/time#>.

# Scoped negation: an employee with no known manager.
{ ?x a v:Employee. ?SCOPE log:notIncludes { ?x v:manager ?m } } => { ?x a v:Unmanaged }.

# Collecting: the members of a team, and how many there are.
{ ?team a v:Team.
  (?p { ?p v:memberOf ?team } ?members) log:collectAllIn ?SCOPE.
  ?members list:length ?n
} => { ?team v:size ?n }.

# The clock.
{ "" time:localTime ?t } => { v:run v:at ?t }.

log:notIncludes succeeds when the formula is not found in the scope it is asked about. Add a manager for Bob and the conclusion “Bob is unmanaged” becomes false. That is non-monotonic: more facts, fewer conclusions. log:collectAllIn and log:forAllIn are non-monotonic in the same way. time:localTime returns the current time, so its answer depends on when you ask.

Tiramemsu treats these three kinds differently:

Why the refusals: chapter 6. In short, a stored conclusion is kept honest by its supports. Supports can be retracted. A fact that was absent cannot be, so nothing would retract the conclusion when that fact arrives.

Backward rules

<= writes a rule the other way round: the head is on the left. A backward rule is not run eagerly. It is used on demand, when another rule’s body asks for its head. This suits recursive definitions that would otherwise flood the result:

ancestors.n3

@prefix v: <urn:tiramemsu:v:>.

{ ?x v:ancestor ?y } <= { ?x v:parent ?y }.
{ ?x v:ancestor ?z } <= { ?x v:parent ?y. ?y v:ancestor ?z }.

# Only this forward rule produces conclusions. It asks for ancestors on demand.
{ ?x v:ancestor v:ada } => { ?x a v:AdaDescendant }.

In tiramemsu, backward rules run over the statements loaded for the run, never over the whole store. Chapter 3 explains what gets loaded.

Inference fuses

A rule whose head is false is an inference fuse. If its body ever matches, the facts contradict each other:

fuse.n3

@prefix v: <urn:tiramemsu:v:>.

{ ?x a v:Cat. ?x a v:Dog } => false.

reason reports a fired fuse as a contradiction, naming the rule and the instance that fired it. materialize stops before writing anything. Recipe 5 uses a fuse as a consistency gate.

What the reasoner returns

For every conclusion eyeron returns the rule that produced it, the premises it matched and the variable bindings. It also reports whether it finished or hit one of its limits, and whether a fuse fired. Tiramemsu turns premises back into statement ids. A conclusion’s proof looks like { rule_set, rule: 0, premises: [e1] }. On request, eyeron’s own N3 proof text comes along too.

Try it

Load the fact into a memory, keep the rule in its own file, and ask the command line. Here the fact is in a Turtle file, socrates.ttl, holding <urn:tiramemsu:v:socrates> a <urn:tiramemsu:v:Human> .

mortality.n3

@prefix v: <urn:tiramemsu:v:>.

{ ?x a v:Human } => { ?x a v:Mortal }.

tm create memory.db
tm import memory.db socrates.ttl
tm reason memory.db --rules mortality.n3
# (v:socrates rdf:type v:Mortal)   rule 0   premises [e1]

The rule file holds only rules. The facts come from memory. The next chapter shows exactly what a rule sees there.