-
Notifications
You must be signed in to change notification settings - Fork 5
/
index.html
231 lines (211 loc) · 9.81 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
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
223
224
225
226
227
228
229
230
231
<!DOCTYPE html>
<html lang="en">
<head>
<!-- standard metadata -->
<meta charset="utf-8" />
<meta name="description" content="Fitch-style proof editor and checker" />
<meta name="author" content="Kevin C. Klement" />
<meta name="copyright" content="© Kevin C. Klement" />
<meta name="keywords" content="logic,proof,deduction" />
<!-- facebook opengraph stuff -->
<meta property="og:title" content="Fitch-style proof editor and checker" />
<meta property="og:image" content="sample.png" />
<meta property="og:description" content="Fitch-style proof proof editor and checker" />
<!-- if mobile ready -->
<meta name="viewport" content="width=device-width, initial-scale=1" />
<meta name="apple-mobile-web-app-capable" content="yes" />
<meta name="mobile-web-app-capable" content="yes" />
<!-- web icon -->
<link rel="shortcut icon" href="favicon.ico" type="image/x-icon" />
<title>Natural deduction proof editor and checker</title>
<!-- page style from https://github.com/dhg/Skeleton -->
<link rel="stylesheet" href="normalize.css">
<link rel="stylesheet" href="skeleton.css">
<link href="https://fonts.googleapis.com/css?family=Noto+Sans" rel="stylesheet" type="text/css">
<style>
body {font-family: "Noto Sans";}
a, a:hover, a:visited, a:focus, a:active {color: #0c1c8c; text-decoration: none; font-weight: bold ;}
label, legend { display: inline-block; }
</style>
<!-- css file -->
<link rel="stylesheet" type="text/css" href="proofs.css" />
<!-- javascript file -->
<script type="text/javascript" charset="utf-8" src="ajax.js"></script>
<script type="text/javascript" charset="utf-8" src="syntax.js"></script>
<script type="text/javascript" charset="utf-8" src="proofs.js"></script>
<!-- font awesome -->
<!-- <script src="https://use.fontawesome.com/b8ae54b59e.js"></script> -->
<script type="text/javascript">
function createProb() {
predicateSettings = (document.getElementById("folradio").checked);
var pstr = document.getElementById("probpremises").value;
pstr = pstr.replace(/^[,;\s]*/,'');
pstr = pstr.replace(/[,;\s]*$/,'');
var prems = pstr.split(/[,;\s]*[,;][,;\s]*/);
var sofar = [];
for (var a=0; a<prems.length; a++) {
if (prems[a] != '') {
var w = parseIt(fixWffInputStr(prems[a]));
if (!(w.isWellFormed)) {
alert('Premise ' + (a+1) + ', ' + fixWffInputStr(prems[a]) + ', is not well formed.');
return;
}
if ((predicateSettings) && (!(w.allFreeVars.length == 0))) {
alert('Premise ' + (a+1) + ' is not closed.');
return;
}
sofar.push({
"wffstr": wffToString(w, false),
"jstr": "Pr"
});
}
}
var conc = fixWffInputStr(document.getElementById("probconc").value);
var cw = parseIt(conc);
if (!(cw.isWellFormed)) {
alert('The conclusion ' + fixWffInputStr(conc) + ', is not well formed.');
return;
}
if ((predicateSettings) && (!(cw.allFreeVars.length == 0))) {
alert('The conclusion is not closed.');
return;
}
document.getElementById("problabel").style.display = "block";
document.getElementById("proofdetails").style.display = "block";
var probstr = '';
for (var k=0; k<sofar.length; k++) {
probstr += prettyStr(sofar[k].wffstr);
if ((k+1) != sofar.length) {
probstr += ', ';
}
}
document.getElementById("proofdetails").innerHTML = "Construct a proof for the argument: " + probstr + " ∴ " + wffToString(cw, true);
var tp = document.getElementById("theproof");
tp.innerHTML = '';
makeProof(tp, sofar, wffToString(cw, false));
}
</script>
<style type="text/css">
#probpremises {
width: 35em;
}
#key td:first-child {
text-align: right;
}
#key td {
height: 3ex;
}
#symkey td:first-child {
text-align: right;
padding-right: 0.5em;
}
.tt {
font-family: monospace;
font-size: 120%;
}
</style>
</head>
<body>
<div class="container">
<div class="row">
<div class="twelve columns" style="margin-top: 5%">
<h1>Natural deduction proof editor and checker</h1>
<p>This is a demo of a proof checker for Fitch-style natural
deduction systems found in many popular introductory logic
textbooks. The specific system used here is the one found in
<em><a href="https://forallx.openlogicproject.org/">forall x:
Calgary</a></em>. (Although based on <em><a
href="https://www.fecundity.com/logic/">forall x: an Introduction
to Formal Logic</a></em>, the proof system in that original
version differs from the one used here and in <em>forall x:
Calgary</em>. However, the system also supports the rules used in
the <em><a
href="https://www.homepages.ucl.ac.uk/~uctytbu/OERs.html">forall
x: Cambridge</a></em> remix.)</p>
</div>
</div>
<div class="row">
<div class="eight columns">
<h3>Create a new problem</h3>
Select if TFL or FOL syntax:<br />
<input type="radio" name="tflfol" id="tflradio" checked /> <label for="tflradio">TFL</label>
<input type="radio" name="tflfol" id="folradio" /> <label for="folradio">FOL</label><br />
Premises (separate with “,” or “;”):<br />
<input id="probpremises" /><br />
Conclusion:<br />
<input id="probconc" /><br />
<button type="button" onclick="createProb();" >create problem</button><br /><br />
<h3 id="problabel" style="display: none;">Proof:</h3>
<p id="proofdetails" style="display: none;"></p>
<div id="theproof"></div>
<h3>Sample exercise sets</h3>
<ul>
<li><a href="tfl-exs.html">Sample Truth-Functional Logic exercises</a> (Chap. 15, ex. C; Chap. 17, ex. B)</li>
<li><a href="fol-exs.html">Sample First-Order Logic exercises</a> (Chap. 32, ex. E; Chap. 34, ex. A)</li>
</ul>
<h3>Instructions</h3>
<table id="symkey">
<tr><td>TFL atomic sentences:<br />(single uppercase letters)</td><td><span class="tt">A, B, X, etc.</span></td></tr>
<tr><td>FOL atomic sentences:<br />(single uppercase letters
<i>other than A or E</i> followed by<br /> lowercase letters a–w
without parentheses, or identities)</td><td><span class="tt">Pa,
Fcdc, a
= d, etc.</span></td></tr>
<tr><td>For negation you may use any of the symbols:</td><td> <span class="tt">¬ ~ ∼ - −</span></td></tr>
<tr><td>For conjunction you may use any of the symbols:</td><td> <span class="tt">∧ ^ & . · *</span></td></tr>
<tr><td>For disjunction you may use any of the symbols:</td><td> <span class="tt">∨ v</span></td></tr>
<tr><td>For the biconditional you may use any of the symbols:</td><td> <span class="tt">↔ ≡ <-> <></span> (or in TFL only: <span class="tt">=</span>)</td></tr>
<tr><td>For the conditional you may use any of the symbols:</td><td> <span class="tt">→ ⇒ ⊃ -> ></span></td></tr>
<tr><td>For the universal quantifier (FOL only), you may use any of the symbols:</td><td> <span class="tt">∀x (∀x) Ax (Ax) (x) ⋀x</span></tr>
<tr><td>For the existential quantifier (FOL only), you may use any of the symbols:</td><td> <span class="tt">∃x (∃x) Ex (Ex) ⋁x</span></tr>
<tr><td>For a contradiction you may use any of the symbols:</td><td> <span class="tt"> ⊥ XX #</span></td></tr>
</table>
<p>The following buttons do the following things:</p>
<table id="key">
<tr><td><a>×</a></td><td>= delete this line</td></tr>
<tr><td><a><img src="new.png" alt="|+"/></a></td><td>= add a line below this one</td></tr>
<tr><td><a><img src="newsp.png" alt="||+" /></a></td><td>= add a new subproof below this line</td></tr>
<tr><td><a><img src="newb.png" alt="<+" /></a></td><td>= add a new line below this subproof to the parent subproof</td></tr>
<tr><td><a><img src="newspb.png" alt="<|+" /></a></td><td>= add a new subproof below this subproof to the parent subproof</td></tr>
</table>
<p>Apart from premises and assumptions, each line has a cell immediately to its right for entering the justifcation. Click on it to enter the justification as, e.g. “&I 1,2”.</p>
<p>Hopefully it is otherwise more or less obvious how to use it.</p>
<p class="footer">The PHP, JavaScript, HTML and CSS source for this page is licensed under the <a href="https://www.gnu.org/licenses/gpl-3.0.en.html">GNU General Purpose License (GPL) v3</a>. Download it <a href="https://github.com/OpenLogicProject/fitch-checker">here</a>.
</div>
<div class="four columns">
<h2>Rules</h2>
<h5>Basic rules</h5>
<img src="rules/r.svg"><br/>
<img src="rules/ai.svg">
<img src="rules/ae.svg">
<img src="rules/oi.svg">
<img src="rules/oe.svg">
<img src="rules/ci.svg">
<img src="rules/ce.svg">
<img src="rules/bi.svg">
<img src="rules/be.svg">
<img src="rules/ni.svg">
<img src="rules/ne.svg">
<img src="rules/xp.svg">
<img src="rules/ip.svg">
<img src="rules/Ai.svg">
<img src="rules/Ae.svg">
<img src="rules/Ei.svg">
<img src="rules/Ee.svg">
<img src="rules/Ii.svg">
<img src="rules/Ie.svg">
<h5>Derived rules</h5>
<img src="rules/ds.svg">
<img src="rules/mt.svg">
<img src="rules/dne.svg">
<img src="rules/lem.svg">
<img src="rules/dem.svg">
<img src="rules/qc.svg">
<h5>Rules for Cambridge</h5>
<img src="rules/ri.svg">
<img src="rules/re.svg">
<img src="rules/tnd.svg">
</div>
</div>
</body>
</html>