Subject, verb and object

All knowledge is just a set of statements

<#pat> <#knows> <#jo> .

### in classical logic: knows(pat,jo)

Everything is identified by URI
Here a local URI but could point to ANY document

Verb known as predicate in the statement
The thing you use a predicate is a Property.
Don't forget the period.

Rules Are Just Statements


#   subject        verb        object
#=============  ==========    ==============
{ ?x :son ?y }      =>        { ?y a :Male }.
{ ?x :son ?y }  log:implies   { ?y a :Male }.

### in classical logic: ∀x ∀y son(x,y) ⇒ male(y)

The terms in braces { } are formulas.

The rule statement relates two formulas.

Queries and Closure

N3 reasoners can give either the result of a query or the deductive closure of an N3 graph
Result of a query

  Given:
    William :likes :spaghetti.

  Query:
    {?x :likes :spaghetti} => {?x :likes :pizza}.

  Result:
    :William :likes :pizza.

A query is a special rule.
Query reasoning provides all the results of the rule marked as query.
The reasoning process can include other rules as well.

Queries and Closure (cont)

Deductive Closure

  Given:
    :William :likes :spaghetti.
    {?x :likes :spaghetti} => {?x :likes :pizza}.

  Closure:
    :William :likes :spaghetti.
    :William :likes :pizza.

The deductive closure is the set of all triples which can be derived from a dataset

We want inter-engine interop which requires proof: SemWave diagram from Tim Berners-Lee

SemWave

We need the full potential of the Semantic Web Databus and Proofbus from Tim Berners-Lee

sweb-bus

EYE, an open source reasoning engine

EYE stands for "Euler Yet another proof Engine" and it is an inference engine supporting logic based proofs.
It performs forward and backward chaining along Euler paths.
The Euler path detection is roughly "don't step in your own steps" to avoid vicious circles so to speak and in that respect there is a similarity with what Leonhard Euler discovered in 1736 for the Koenigsberg Bridge Problem.
The reasoning that EYE is performing is grounded in FOL (First Order Logic).
Keeping a language less powerful than FOL is quite reasonable within an application, but not for the Web, see http://www.w3.org/DesignIssues/Logic.html.
Open source project hosted at https://github.com/josd/eye.

Detailed design of EYE

N3 (Notation 3) parser
N3Logic to N3P (Notation 3 P-code) compiler
EAM (Euler Abstract Machine) with Euler path detection to avoid loops and with postponed brake mechanism to run at much increased speed
proof construction using the http://www.w3.org/2000/10/swap/reason vocabulary for proofs
built-ins and support predicates for the above functionalities
EYE Stack

Basic EAM (Euler Abstract Machine)

This is what the basic EAM (Euler Abstract Machine) does in a nutshell:

Select rule P => C
Prove P & NOT(C) (backward chaining) and if it fails backtrack to 1/
If P & NOT(C) assert C (forward chaining) and remove brake
If C = answer(A) and tactic limited-answer stop, else backtrack to 2/
If brake or tactic linear-select stop, else start again at 1/

Forward vs. Backward Chaining

In N3 you can indicate how a rule should be applied:

Forward-chaining:

{?x :likes :Spaghetti} => {?x :likes :Pizza}.

Backward-chaining:

{?x :likes :Pizza} <= {?x :likes :Spaghetti}.

Proof generation

[] a r:Proof, r:Conjunction;
  r:component <#lemma1>;
  r:component <#lemma2>;
  r:gives {
    :Socrates a :Human.
    :Socrates a :Mortal.
  }.

...

using lemmata to avoid "exponential" length of proofs
lemmata also enable "multi-agent proofs"

Proof generation (cont)

<#lemma5> a r:Inference;
  r:gives { :Socrates a :Mortal };
  r:evidence ( <#lemma6> <#lemma3> );
  r:binding [ r:variable [ n3:uri "http://josd.github.io/var#x_0"]; r:boundTo [ n3:uri "http://example.org/socrates#Human"]];
  r:binding [ r:variable [ n3:uri "http://josd.github.io/var#x_1"]; r:boundTo [ n3:uri "http://example.org/socrates#Mortal"]];
  r:binding [ r:variable [ n3:uri "http://josd.github.io/var#x_2"]; r:boundTo [ n3:uri "http://example.org/socrates#Socrates"]];
  r:rule <#lemma7>.

<#lemma6> a r:Extraction;
  r:gives { :Human rdfs:subClassOf :Mortal };
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/socrates/socrates.n3>].

<#lemma7> a r:Extraction;
  r:gives {
    @forAll var:x_0, var:x_1, var:x_2. {var:x_0 rdfs:subClassOf var:x_1.
     var:x_2 a var:x_0} => {var:x_2 a var:x_1}.
  };
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/socrates/socrates.n3>].

Deep just-in-time indexing

Just-in-time indexing means that indexes are generated on the first call to a predicate if index might help
Deep indexes allow for efficient lookup of arbitrary terms

Built-ins

Predicates with special meanings

"Traditional" N3 built-ins: https://www.w3.org/2000/10/swap/doc/CwmBuiltins

"New" built-ins are currently discussed in the W3C N3 community group

List of EYE built-ins: https://github.com/josd/eye/blob/master/eye-builtins.n3

EYE command line interface

Usage: eye <options>* <data>* <query>*

<data>
    [--n3] <uri>                    N3 triples and rules
    --blogic <uri>                  RDF surfaces
    --n3p <uri>                     N3P intermediate
    --proof <uri>                   N3 proof lemmas
    --turtle <uri>                  Turtle triples
<query>
    --entail <rdf-graph>            output true if RDF graph is entailed
    --not-entail <rdf-graph>        output true if RDF graph is not entailed
    --pass                          output deductive closure
    --pass-all                      output deductive closure plus rules
    --pass-all-ground               ground the rules and run --pass-all
    --pass-only-new                 output only new derived triples
    --query <n3-query>              output filtered with filter rules

EYE command line interface (cont)

<options>
    --csv-separator <separator>     CSV separator such as , or ;
    --debug                         output debug info on stderr
    --debug-cnt                     output debug info about counters on stderr
    --debug-djiti                   output debug info about DJITI on stderr
    --debug-pvm                     output debug info about PVM code on stderr
    --help                          show help info
    --hmac-key <key>                HMAC key used in e:hmac-sha built-in
    --ignore-inference-fuse         do not halt in case of inference fuse
    --image <pvm-file>              output all <data> and all code to <pvm-file>
    --intermediate <n3p-file>       output all <data> to <n3p-file>
    --license                       show license info
    --multi-query                   go into query answer loop
    --no-distinct-input             no distinct triples in the input
    --no-distinct-output            no distinct answers in the output
    --no-numerals                   no numerals in the output
    --no-qnames                     no qnames in the output
    --no-qvars                      no qvars in the output
    --no-ucall                      no extended unifier for forward rules
    --nope                          no proof explanation
    --profile                       output profile info on stderr
    --quantify <prefix>             quantify uris with <prefix> in the output
    --quiet                         quiet mode
    --random-seed                   create random seed for e:random built-in
    --restricted                    restricting to core built-ins
    --rule-histogram                output rule histogram info on stderr
    --skolem-genid <genid>          use <genid> in Skolem IRIs
    --source <file>                 read command line arguments from <file>
    --statistics                    output statistics info on stderr
    --strings                       output log:outputString objects on stdout
    --tactic limited-answer <nr>    give only a limited number of answers
    --tactic limited-brake <nr>     take only a limited number of brakes
    --tactic limited-step <nr>      take only a limited number of steps
    --tactic limited-witness <nr>   use only a limited number of witnesses
    --tactic linear-select          select each rule only once
    --version                       show version info
    --warn                          output warning info on stderr
    --wcache <uri> <file>           to tell that <uri> is cached as <file>

Use case GPS4IntegratedCare

The GPS4IntegratedCare project objective is Automatic generation of dynamic and personalized care workflows

Technologies used:

Semantic Web Language (JSON-LD, Turtle, N3)
Reasoning Engine (EYE)

Goal driven Parallel Sequences (GPS):

Inspired by Linear Logic
"In linear logic we are instead concerned with the change of truth with a change of state. We model this in a very simple way: when an inference rule is applied we consume the propositions used as premises and produce the propositions in the conclusions, thereby effecting an overall change in state."
Implemented in GPS plugin for EYE

Use case GPS4IntegratedCare lessons learned

The project worked out fine, but the architecture is centralized around a single smart workflow engine and that is really not scalable.

The proposal is to address the scalability with MAP

Multi-Agent Proofs (MAP):

Multiple agents can work together by using their own knowledge/logic/data and proofs made by other agents.
The proofs are guaranteeing a transparent and accountable way of working and they only disclose what is relevant, so there is no need to have an "All knowledge is contained in here" (what I learned from Tim Berners-Lee).

This is just a proposal with a proof of concept in which agent1 and agent2 are GPS agents and agent2 reaches his goal thanks to the lemmata made by agent1.

Multi-Agent Proofs: Agent2 reaches his goal thanks to the lemmata made by Agent1

Agent2-proof makes use of lemma9 from Agent1-proof

<#lemma13> a r:Extraction;
  r:gives {
    <http://josd.github.io/eye/reasoning/map/agent1-proof.n3#lemma9> a r:Inference.
  };
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/map/agent1-proof.n3>].

<#lemma14> a r:Extraction;
  r:gives {
    <http://josd.github.io/eye/reasoning/map/agent1-proof.n3#lemma9> r:gives {
      :map-BE gps:description ({:i1 :location :Gent} true {:i1 :location :Brugge} :drive_gent_brugge 1500.0 0.006 0.96 0.99)
    }.
  };
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/map/agent1-proof.n3>].

Reverse the burden of proof

The burden of proof is now on the server:

the server has to find out why he should do the job for the client
but there is no omniscient server

Reverse the burden of proof:

the client provides a proof
the server checks that proof
if the proof is fine the server does the job for the client

This is much more scalable but requires client side reasoning + proof generation

The proof could be provided as HTTP GET payload

Testing: Examples and Test Cases

bayesian networks: ccd, nbbn, swet
control systems: cs
description logic: bmt, dt, edt, entail, gedcom, graph, h2o, RDF plus OWL (source)
ershovian compilation: preduction
extensible imaging: lldm
logic programming: 4color, de, dp, dpe, gcc, hanoi, lee, socrates, witch, zebra
markovian networks: mmln
mathematical reasoning: complex, equation, fibonacci, padovan, pi, polygon, polynomial, prime, tak
neural networks: fcm, fgcm
quantum computation: dqc
universal machines: turing, usm
workflow composers: gps, map, resto, restpath, twf

Advanced Clinical Applications

ACAS

Basic MONADIC Benchmark

       triples   cycles |         cwm         eye        jena
                        |       [sec]       [sec]       [sec]
------------------------|------------------------------------
        10,000    1,518 |      15.400       0.420       3.200
       100,000      645 |      99.860       2.190       9.310
     1,000,000      380 |   1,094.860      21.170      75.380
    10,000,000      480 |  (OutOfMem)     231.610     853.060
   100,000,000      480 |               2,640.580   9,217.800
 1,000,000,000      431 |              32,474.540  (OutOfMem)

Test environment:

Linux 4.0.5 x86_64
processor	: 0
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
processor	: 1
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
processor	: 2
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
processor	: 3
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
MemTotal:       264163268 kB


Reference:

http://eulersharp.sourceforge.net/2014/11bmb/README.md

Deep taxonomy benchmark

         depth |         cwm         eye      hermit       jdrew        jena
               |       [sec]       [sec]       [sec]       [sec]       [sec]
---------------|------------------------------------------------------------
            10 |       0.160       0.018       0.055       0.130       0.047
           100 |       1.050       0.022       1.040       0.200       0.422
         1,000 |      65.930       0.063       3.580       0.870       9.302
        10,000 |   7,298.000       0.482     310.510      18.680   2,597.242
       100,000 | 732,974.070       4.808  (OutOfMem)   1,875.000  (OutOfMem)
     1,000,000 |  (848 days)      48.434              (OutOfMem)


Test environment:

Linux 4.0.5 x86_64
processor	: 0
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
processor	: 1
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
processor	: 2
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
processor	: 3
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
MemTotal:       264163268 kB


Reference:

http://ruleml.org/WellnessRules/files/WellnessRulesN3-2009-11-10.pdf

RESTdesc Composition Benchmark

        length |         cwm         eye
               |       [sec]       [sec]
---------------|------------------------
             2 |       0.188       0.029
             4 |       0.371       0.032
             8 |       1.004       0.038
            16 |       3.504       0.053
            32 |      13.968       0.085
            64 |      58.689       0.157
           128 |     251.361       0.344
           256 |   1,081.179       0.936
           512 | (MaxRecurs)       2.894
         1,024 |                   9.764


Test environment:

Linux 4.0.5 x86_64
processor	: 0
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
processor	: 1
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
processor	: 2
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
processor	: 3
model name	: Intel(R) Xeon(R) CPU E5-2665 0 @ 2.40GHz
MemTotal:       264163268 kB


Reference:

https://github.com/RubenVerborgh/RESTdesc-Composition-Benchmark

Building Semantic Web reasoning engines

Context is Semantic Web (some slides from Tim Berners-Lee, Doerthe Arndt and William Van Woensel)