-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
87 lines (75 loc) · 3.34 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
<html>
<head>
<meta charset="utf-8">
<script type="text/javascript" src="https://cdnjs.cloudflare.com/ajax/libs/vis/4.21.0/vis.js"></script>
<link href="https://cdnjs.cloudflare.com/ajax/libs/vis/4.21.0/vis-network.min.css" rel="stylesheet" type="text/css" />
<link rel="stylesheet" href="/style.css" />
<style type="text/css">
#networkbox {
width: 700px;
height: 400px;
border: 1px solid lightgray;
}
</style>
</head>
<body>
<h1>First-order logic for graphs</h1>
<center><div id="networkbox"></div></center>
<div id="repl-1" class="repl"></div>
<p>Type in some expressions in first-order logic to select nodes of the graph that have different properties. The syntax is like this:</p>
<ul>
<li><code>E</code> stands for "there exists".</li>
<li><code>A</code> stands for "for all".</li>
<li><code>y</code> is a free variable standing in for the selected nodes.</li>
<li><code>x0,...,x99</code> are variable names that you can use for bound variables.</li>
<li><code>&</code> means "and", <code>|</code> means "or" and <code>~</code> means "not".</li>
<li><code>eq(a,b)</code> means "<code>a</code> and <code>b</code> are equal."</li>
<li><code>R(a,b)</code> means "there is an arrow from <code>a</code> to <code>b</code>."</li>
<li>You can also use parentheses.</li>
</ul>
Here are some examples of predicates that you could try out:
<ul>
<li><code>eq(y,y)</code> will just select all of the nodes, since every node equals itself!</li>
<li><code>Ex0 R(y,x0)</code> says "there exists some node that this node points to". So it will select all nodes that point to at least one other node.</li>
<li><code>R(y,y)</code> will select all of the nodes that have an arrow to themselves.</li>
<li><code>Ex0 Ex1 R(y,x0) & R(y,x1) & ~eq(x0,x1)</code> will select each node that points to <i>at least two different nodes</i>.</li>
</ul>
Try the following puzzles. For each puzzle, you should try to write a predicate that is satisfied <i>only by the blue nodes</i>.
<ol id="levels-list">
</ol>
<script type="text/javascript" src="/fol.js"></script>
<script type="text/javascript" src="/mvc.js"></script>
<script type="text/javascript" src="/repl.js"></script>
<script type="text/javascript">
m = new Model()
m.runRandomGraph(20, 0.1)
v = new View()
v.visNodesList(20)
v.visEdgesList(m.edglist)
c = new Controller(m, v)
c.randomize()
var levelsList = document.getElementById("levels-list");
for (let n in levels) {
var level = levels[n];
var levelElt = document.createElement("li");
var clickable = document.createElement("a");
var levelMarker = document.createElement("a");
levelMarker.textContent = " ❓"
levelMarker.id = `level-marker-${n}`
clickable.textContent = level.name;
clickable.href = `javascript:c.runLevel(levels[${n}])`;
levelElt.appendChild(clickable);
levelElt.appendChild(levelMarker);
levelsList.appendChild(levelElt)
}
buildREPL(1, "Type first-order logic predicates to select graph nodes.", ">")
registerREPL((n, strin) => {
putLineToREPL(`> ${strin}`, n);
var done = c.tryPredicate(strin);
if (done) {
putLineToREPL("You've solved this puzzle! Good job!", n)
}
}, 1)
</script>
</body>
</html>