forked from eyereasoner/eye
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
128 lines (111 loc) · 8 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<title>EYE</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="stylesheet" href="https://josd.github.io/StyleSheets/style.css" type="text/css" />
<link rel="shortcut icon" href="https://josd.github.io/images/favicon.ico" type="image/vnd.microsoft.icon" />
<style type="text/css">a:hover {background:#ffa;}</style>
</head>
<body xml:lang="en" lang="en">
<h1 id="euler-yet-another-proof-engine-eye">Euler Yet another proof Engine - EYE</h1>
<p><img align="left" src="https://josd.github.io/images/eye.png" alt="EYE"/>
<a href="https://github.com/eyereasoner/eye">EYE</a> is a reasoning engine supporting the <a href="http://www.w3.org/DesignIssues/diagrams/sweb-stack/2006a">Semantic Web layers</a>.
It performs forward and backward chaining along Euler paths.
Via <a href="https://w3c.github.io/N3/spec/">N3</a> it is interoperable with <a href="http://www.w3.org/2000/10/swap/doc/cwm">Cwm</a>.<br/>
Forward chaining is applied for rules using <code>=></code> in <a href="https://w3c.github.io/N3/spec/">N3</a> and backward chaining
is applied for rules using <code><=</code> in <a href="https://w3c.github.io/N3/spec/">N3</a> which one can imagine as built-ins.
Euler paths are roughly <em>"don't step in your own steps"</em> which is inspired by
what <a href="https://en.wikipedia.org/wiki/Leonhard_Euler">Leonhard Euler</a> discovered in 1736 for the <a href="http://mathworld.wolfram.com/KoenigsbergBridgeProblem.html">Königsberg Bridge Problem</a>.
EYE sees the rule <code>P => C</code> as <code>P & ˜C => C</code>.</p>
<h2 id="architecture-and-design">Architecture and design</h2>
<p>The <strong>EYE stack</strong> comprises the following Software and Machines:</p>
<img src="https://josd.github.io/images/EYE-stack.png" width="480" height="400" alt="EYE-stack"/>
<p>This is what the basic <strong>EAM (Euler Abstract Machine)</strong> does in a nutshell:
<ol>
<li>Select rule <code>P => C</code></li>
<li>Prove <code>P & ˜C</code> (backward chaining) and if it fails backtrack to 1.</li>
<li>If <code>P & ˜C</code> assert <code>C</code> (forward chaining) and remove brake</li>
<li>If <code>C = answer(A)</code> and tactic limited-answer stop, else backtrack to 2.</li>
<li>If brake or tactic linear-select stop, else start again at 1.</li>
</ol></p>
<h2 id="eye-unifying-logic">EYE Unifying Logic</h2>
<ul>
<li>Design Issues of Tim Berners-Lee: <a href="https://www.w3.org/DesignIssues/Logic.html">The Semantic Web as a language of logic</a></li>
<li>PhD thesis of Dörthe Arndt: <a href="https://github.com/doerthe/PhD/blob/master/main.pdf">Notation3 as the Unifying Logic for the Semantic Web</a></li>
<li>Proposed built-ins of w3c N3: <a href="https://w3c.github.io/N3/ns/">Vocabulary Definitions</a></li>
</ul>
<h2 id="eye-reasoning">EYE Reasoning</h2>
<p>Running the Semantic Web Databus and Proofbus from <a href="http://www.w3.org/People/Berners-Lee/">Tim Berners-Lee</a> which is
like a world wide welding machine transforming data into proofs:</p>
<p><img src="https://www.w3.org/DesignIssues/diagrams/sweb-bus.png" width="480" height="400" alt="PDB"/></p>
<h3 id="examples-and-test-cases">Examples and Test Cases</h3>
<ul>
<li>bayesian networks:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/ccd">ccd</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/nbbn">nbbn</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/swet">swet</a></li>
<li>control systems:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/cs">cs</a></li>
<li>description logic:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/bmt">bmt</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/dt">dt</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/edt">edt</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/entail">entail</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/gedcom">gedcom</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/graph">graph</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/h2o">h2o</a>,
<a href="reasoning/rpo/">RDF plus OWL</a>
(<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/rpo">source</a>)</li>
<li>ershovian compilation:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/preduction">preduction</a></li>
<li>extensible imaging:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/lldm">lldm</a></li>
<li>logic programming:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/4color">4color</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/de">de</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/dp">dp</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/dpe">dpe</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/gcc">gcc</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/hanoi">hanoi</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/lee">lee</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/socrates">socrates</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/witch">witch</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/zebra">zebra</a></li>
<li>markovian networks:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/mmln">mmln</a></li>
<li>mathematical reasoning:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/complex">complex</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/equation">equation</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/fibonacci">fibonacci</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/padovan">padovan</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/pi">pi</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/polygon">polygon</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/polynomial">polynomial</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/prime">prime</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/tak">tak</a></li>
<li>neural networks:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/fcm">fcm</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/fgcm">fgcm</a></li>
<li>quantum computation:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/dqc">dqc</a></li>
<li>universal machines:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/turing">turing</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/usm">usm</a></li>
<li>workflow composers:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/gps">gps</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/map">map</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/resto">resto</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/restpath">restpath</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/twf">twf</a></li>
</ul>
<h2 id="see-also">See also</h2>
<ul>
<li>EYE paper: <a href="https://josd.github.io/Papers/EYE.pdf">Drawing Conclusions from Linked Data on the Web: The EYE Reasoner</a></li>
<li>EYE tutorial: <a href="https://n3.restdesc.org/">Semantic Web Reasoning With EYE</a></li>
<li>EYE talk: <a href="http://josd.github.io/Talks/2012/04swig/index.html">EYE looking through N3 glasses</a></li>
<li>N3 talk: <a href="https://josd.github.io/temp/Notation3_A_practical_introduction.pdf">Notation3 Logic: A Practical Introduction</a></li>
</ul>
</body>
</html>