/
gentzen.html
222 lines (210 loc) · 10.2 KB
/
gentzen.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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
<html>
<head>
<title>Gentzen</title>
<link rel="stylesheet" type="text/css" href="semantic/dist/semantic.min.css">
<script src="https://code.jquery.com/jquery-3.1.1.min.js" integrity="sha256-hVVnYaiADRTO2PzUGmuLJr8BLUSjGIZsDYGmIJLv2b8=" crossorigin="anonymous"></script>
<script src="semantic/dist/semantic.min.js"></script>
<link rel="stylesheet" type="text/css" href="dist/Treant.css">
<script src="dist/vendor/raphael.js"></script>
<script src="dist/Treant.js"></script>
<script src="dist/bundle.js"></script>
<style>
code, kbd, pre, samp, .proposition {
font-family: Verdana, monospace !important;
font-size: 0.8em !important;
}
</style>
</head>
<body>
<div class="ui container">
<div class="ui header">
<h1>Automated Propositional Logic Proofs using Gentzen Deduction Trees</h1>
<div class="sub header">
by Dylan Jager-Kujawa
</div>
</div>
<div class="ui top attached segment">
<div class="ui header">
Enter an Expression
<div class="ui right floated icon image">
<a id="btnInputHelp" class="ui right circular icon button">
<i class="help icon"></i>
</a>
</div>
</div>
<div class="ui form">
<div class="ui fluid action input">
<input type="text" id="txtProposition" class="proposition" placeholder="e.g., (P -> Q) -> (!Q -> !P)">
<button id="btnParse" class="ui button">Parse</button>
</div>
<a id="btnPermalink" style="display: none">Permalink to this query</a>
</div>
</div>
<div class="ui bottom attached segment">
<div class="header">
<h4>Parsed, Fully-Parenthesized Expression</h4>
</div>
<div class="ui message">
<code id="codeParsed">
e.g., ((P -> Q) -> (!Q -> !P))
</code>
</div>
</div>
<div class="ui raised segment">
<div class="ui header">
Deduction Tree
<div id="result" class="sub header">
<a id="btnResultHelp">What does this mean?</a>
</div>
</div>
<div class="ui center aligned content">
<div id="tree-simple"></div>
</div>
</div>
</div>
<div id="mdlInputHelp" class="ui modal">
<div class="ui three column stackable divided padded grid">
<div class="row">
<div class="column">
<div class="ui header">
Propositional Symbols
</div>
<div class="ui content">
<p>Propositional symbols must begin with a letter, and can be followed by letters or numbers. For example, "Rainy", "Car1", etc.</p>
</div>
</div>
<div class="column">
<div class="ui header">
Operators
</div>
<div class="ui content">
<p>The following operators are recognized:</p>
<div class="ui list">
<div class="item"><i class="right triangle icon"></i> ! (not)</div>
<div class="item"><i class="right triangle icon"></i> && (and)</div>
<div class="item"><i class="right triangle icon"></i> || (or)</div>
<div class="item"><i class="right triangle icon"></i> -> (implication)</div>
</div>
<p>Parentheses may be used to group sub-propositions, but make sure they are balanced.</p>
</div>
</div>
<div class="column">
<div class="ui header">
Precedence
</div>
<div class="ui content">
<p>Operator precedence is shown in the list of operators, with higher-precedence operators appearing higher in the list.</p>
<p>Parentheses take precedence over all operators.</p>
<p>If you're unsure if your syntax is correct, verify the parsed expression below.</p>
</div>
</div>
</div>
</div>
</div>
<div id="mdlResultHelp" class="ui modal">
<div class="ui header">
Interpreting the Results
</div>
<div class="ui content">
<p>Results are displayed in a tree, with each node representing a sequent. A sequent is an <b>axiom</b> if its assumptions and conclusions share a common proposition. A node is <b>finished</b> if it is an axiom, or if its assumptions and conclusions consist of only atomic symbols.</p>
<p>All unfinished nodes are <em>expanded</em>, that is to say, inference rules are applied to them to manipulate the propositions between the assumptions and conclusions.</p>
<p>When all nodes in the tree are finished, the deduction tree is complete, and is displayed graphically below. <b>Axioms are highlighted in green. Finished non-axioms are highlighted in red.</b></p>
<hr />
<p>If, once the tree is finished, all <em>leaves</em> of the tree are axioms, then the original proposition is a <b>tautology</b> (i.e. it is always true). If any leaves are not axioms, the original proposition is not a tautology, and any non-axiom leaves contain the counter-examples to disprove it.</p>
<hr />
<p><b>TLDR:</b> If all your tree's leaves are <b style="color: green;">green</b>, the proposition is true. If any leaves are <b style="color: red">red</b>, it is false, and the red leaves are the counterexamples.</p>
<p>For more information, check the <a href="https://github.com/Kujawadl/Gentzen/wiki" target="_blank">Gentzen wiki</a>.</p>
</div>
</div>
<div id="mdlPermalink" class="ui small modal">
<div class="ui header">Permalink</div>
<div class="ui content">
<form class="ui form">
<div class="field">
<label>Use this link to return to this query at a later time:</label>
<input type="text" id="txtPermalink" readonly>
</div>
</form>
</div>
</div>
<script>
var proposition;
var gentzenTree;
var chart;
function drawTree() {
if (gentzenTree !== undefined && gentzenTree !== null) {
chart = new Treant({
chart: {
container: "#tree-simple",
connectors: {
style: {
"arrow-end": "classic-wide-long"
}
}
},
nodeStructure: gentzenTree.root
}, undefined, $);
}
};
// Proposition input
$("#txtProposition").focus();
$("#txtProposition").keypress(function(e){
if (e.keyCode==13) { $("#btnParse").click() };
});
$("#txtProposition").keyup(function(e) {
if (this.value != "") {
$("#btnPermalink").show();
} else {
$("#btnPermalink").hide();
}
});
// Help modals
$(".ui.modal").modal({
transition: "scale"
});
$("#btnInputHelp").click(function() {
$("#mdlInputHelp").modal("show");
});
$("#btnResultHelp").click(function() {
$("#mdlResultHelp").modal("show");
});
$("#btnPermalink").click(function() {
$("#txtPermalink").val([
location.protocol,
"//",
location.host,
location.pathname,
"?p=" + encodeURIComponent($("#txtProposition").val())
].join(""));
$("#mdlPermalink").modal("show");
$("#txtPermalink").focus();
});
$("#txtPermalink").focus(function() {
$(this).select();
});
// Parse button
$("#btnParse").click(function() {
proposition = undefined;
gentzenTree = undefined;
!chart || chart.destroy();
try {
proposition = new Gentzen.Proposition($("#txtProposition").val());
$("#codeParsed").html(proposition.toString()).parent().removeClass("error");
gentzenTree = new Gentzen.GentzenTree(proposition);
drawTree();
} catch (ex) {
console.error(ex);
$("#codeParsed").html(ex.message).parent().addClass("error");
}
});
// Resize tree with window
$(window).resize(drawTree);
// Get initial value from query string if available
var urlParams = new URLSearchParams(window.location.search);
if (urlParams.has("p")) {
$("#txtProposition").val(decodeURIComponent(urlParams.get("p")));
$("#btnParse").click();
}
</script>
</body>
</html>