Euler Yet another proof Engine - EYE

EYE

DOI

EYE is a reasoning engine supporting the Semantic Web layers and implementing Notation3.

EYE performs forward and backward chaining along Euler paths.  Forward chaining is applied for rules using => in Notation3 and backward chaining is applied for rules using <= in Notation3 which one can imagine as user defined built-ins. Euler paths are roughly "don't step in your own steps" which is inspired by what Leonhard Euler discovered in 1736 for the Königsberg Bridge Problem.

Installation

  - Install SWI-Prolog from http://www.swi-prolog.org/Download.html

  - Test the SWI-Prolog installation via command line swipl --version and it should return the installed version number.

  - Run the installation script install.sh [--prefix=Prefix].  The default prefix is /usr/local.  This will
    
      - create the EYE image file at $prefix/lib/eye.pvm
      - create the EYE launch script eye ub $prefix/bin/eye

Test the EYE installation via command line eye --version and it should return the version which is in the file VERSION.

Usage

Create a test Notation3 file. We use the file socrates.n3 as example:

$ cat socrates.n3
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix : <http://example.org/socrates#>.

:Socrates a :Human.
:Human rdfs:subClassOf :Mortal.

{
    ?S a ?A .
    ?A rdfs:subClassOf ?B . 
} 
=> 
{
    ?S a ?B .
} .

Run the EYE reasoner without proof explanation, in quiet mode and passing all deductive closures
to the output:

$ eye --nope --quiet --pass socrates.n3
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix : <http://example.org/socrates#>.

:Socrates a :Human.
:Socrates a :Mortal.
:Human rdfs:subClassOf :Mortal.

Tutorial and example scripts

  - Eye command line arguments and flags
  - Eye reasoning examples and test cases
  - Notation3 by example
  - RDF Surfaces aka BLOGIC
  - Running EYE using Docker

Online versions of EYE

  - Notation3 Editor https://editor.notation3.org/
  - Semantic Web Reasoning With N3 https://n3.restdesc.org/rules/executing-rules/
  - Eyebrow https://github.com/eyereasoner/eyebrow

References

  - Home page of EYE https://eyereasoner.github.io/eye/
  - Former home page of EYE http://eulersharp.sourceforge.net/
  - Notation3 W3C Draft Community Group Report https://w3c.github.io/N3/spec/
  - More EYE tools and scripts https://github.com/eyereasoner/
  - Design Issues of Tim Berners-Lee: The Semantic Web as a language of logic
  - PhD thesis of Dörthe Arndt: Notation3 as the Unifying Logic for the Semantic Web

Publications

Verborgh, R. , De Roo, J. : Drawing Conclusions from Linked Data on the Web: The EYE Reasoner. IEEE Software (2015) Online Version

License & copyright

MIT License
