-
Notifications
You must be signed in to change notification settings - Fork 17
/
index.html
143 lines (124 loc) · 8.86 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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
<?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="https://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="https://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="unifying-logic">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/reports/20230703/builtins.html">Notation3 Builtin Functions</a></li>
</ul>
<h2 id="explainable-reasoning">Explainable Reasoning</h2>
<p>Running the Semantic Web Databus and Proofbus from <a href="https://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="eye-reasoning-assumptions">EYE reasoning assumptions</h3>
<ul>
<li>N3 rules can only have quickvars and they have rule scope</li>
<li>Quickvars are interpreted universally except for forward rule conclusion-only variables which are interpreted existentially</li>
<li>Blank nodes are interpreted existentially and have document scope</li>
</ul>
</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/acp">acp</a>,
<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/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>graph computation:
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/graph">graph</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/path-discovery">path-discovery</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/dp">dp</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/diamond-property">diamond-property</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/n-queens">n-queens</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/ackermann">ackermann</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/eulers-identity">eulers-identity</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/peano">peano</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/peasant-multiplication">peasant-multiplication</a>,
<a href="https://github.com/eyereasoner/eye/tree/master/reasoning/peasant-power">peasant-power</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/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>
</p>
<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>
<li>N3 editor: <a href="https://editor.notation3.org/">Notation3 Editor</a></li>
</ul>
</body>
</html>