-
Notifications
You must be signed in to change notification settings - Fork 17
/
Copy pathindex.html
158 lines (138 loc) · 9.9 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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
<?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>
<p>For EYE we strive to realize the inherent potential of mathematical reasoning:
<ul>
<li>direct proof: a logical method starting from the statement to be proven (top-down) and known facts or axioms
(bottom-up), working step-by-step from both directions until they meet to form a complete logical argument.</li>
<li>proof by contrapositive: a logical method where you prove that if the conclusion is false, the premise must
also be false, which is logically equivalent to proving the original statement.</li>
<li>proof by contradiction: a logical method where you assume the negation of the statement to be proven,
derive a contradiction, and conclude that the original statement must be true.</li>
<li>proof by cases: a logical method where a statement is proven by dividing it into distinct, exhaustive cases
and demonstrating that the statement holds true in each case.</li>
<li>proof by recursion: a logical method of establishing a result by defining a base case and a recursive step
that derives the solution for larger cases from smaller ones.</li>
</ul>
</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>