forked from wo/tpg
-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.php
176 lines (151 loc) · 7.99 KB
/
index.php
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
<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Tree Proof Generator</title>
<link href="https://fonts.googleapis.com/css?family=M+PLUS+1p:500&display=swap" rel="stylesheet">
<link rel="stylesheet" href="style.css" type="text/css">
</head>
<body>
<div id="main">
<div id="titlebar">
<h2 id="title"><a id="titlelink" href=".">Tree Proof Generator</a></h2>
<a id="githublink" class="hideOnPhone" href="https://www.github.com/wo/tpg/commits/master">Last update: <?=date('d M Y', filemtime('.git/refs/heads/master'))?></a>
</div>
<form id="inputForm" action="." method="get" onsubmit="return false">
<div id="symbolButtonRow">
insert <span class="hideOnTablet">symbol:</span>
<div id="symbolButtons">
<div class="symbutton button formula">¬</div><div class="symbutton button formula">∧</div><div class="symbutton button formula">∨</div><div class="symbutton button formula">→</div><div class="symbutton button formula">↔</div><div class="symbutton button formula">∀</div><div class="symbutton button formula">∃</div><div class="symbutton button formula">□</div><div class="symbutton button formula">◇</div>
</div>
</div>
<div id="proveRow">
<input type="text" size="60" name="flaField" id="flaField" class="formula">
<input type="submit" value="Run" id="proveButton" class="button">
</div>
<div id="accessibilityRow">
<span id="accessibilitySpan">
Accessibility is
<label><input type="checkbox" class="accCheckbox" id="universality" value="∀v∀uRvu"> universal (S5)</label>
<label><input type="checkbox" class="accCheckbox" id="reflexivity" value="∀vRvv"> reflexive</label>
<label><input type="checkbox" class="accCheckbox" id="symmetry" value="∀v∀u(Rvu→Ruv)"> symmetric</label>
<label><input type="checkbox" class="accCheckbox" id="transitivity" value="∀v∀u∀t(Rvu→(Rut→Rvt))"> transitive</label>
<label><input type="checkbox" class="accCheckbox" id="euclidity" value="∀v∀u∀t(Rvu→(Rvt→Rut))"> euclidean</label>
<label><input type="checkbox" class="accCheckbox" id="seriality" value="∀v∃uRvu"> serial</label>
</span>
</div>
</form>
<div id="backtostartpage"><a href=".">back to start page</a></div>
<div id="status"><div id="statusmsg"></div><div id="statusbtn"></div></div>
<div id="model"> </div>
<div id="rootAnchor"> </div>
<?php
$scripts = array("array", "formula", "parser", "prover", "equality", "modelfinder", "sentree", "painter", "index");
if (isset($_GET['debug'])) {
?>
<script>
function log(str, tracelog) {
if (!self.debugWin) debugPopup();
<?php if ($_GET['debug'] == "trace") { ?>
if (tracelog) {
debugWin.document.write("<pre>"+str+"</pre>");
}
<?php } else { ?>
if (!tracelog) {
debugWin.document.write("<pre>"+str+"</pre>");
}
<?php } ?>
}
function debugPopup() {
self.debugWin = self.open("about:blank","debugWin");
if (!self.debugWin) alert("unblock popups!");
}
log("hello, this is the debugging window");
</script>
<?php
foreach ($scripts as $script) {
if (strpos($_GET['debug'], $script) !== false || in_array($_GET['debug'], array("1", "trace"))) {
print "<script type='text/javascript' src='$script.debug.js'></script>\n";
}
else {
print "<script type='text/javascript' src='$script.js'></script>\n";
}
}
}
else {
$allscripts = implode("-", $scripts);
print "<script type='text/javascript' src='$allscripts.js'></script>\n";
}
?>
<div id="intro">
<noscript><p><b>You need to enable JavaScript to use this page.</b></p></noscript>
<p>Enter a formula of standard propositional, predicate, or modal logic. The
page will try to find either a countermodel or
a <a href="https://en.wikipedia.org/wiki/Method_of_analytic_tableau">tree
proof (a.k.a. semantic tableau)</a>. </p>
<p>Examples (click!):</p>
<ul id="exampleList">
<li class="formula"><a href="#(p∨(q∧r))→((p∨q)∧(p∨r))">(p∨(q∧r)) → ((p∨q) ∧ (p∨r))</a></li>
<li class="formula"><a href="#∃y∀x(Fy→Fx)">∃y∀x(Fy → Fx)</a></li>
<li class="formula"><a href="#∃y∃z∀x((Fx→Gy)∧(Gz→Fx))→∀x∃y(Fx↔Gy)">∃y∃z∀x((Fx → Gy) ∧ (Gz → Fx)) → ∀x∃y(Fx ↔ Gy)</a></li>
<li class="formula"><a href="#N(0)∧∀i(N(i)→N(s(i)))→N(s(s(s(0))))">N(0) ∧ ∀i(N(i) → N(s(i))) → N(s(s(s(0))))</a></li>
<li class="formula"><a href="#∀x(∃y(Fy∧x=f(y))→Fx)↔∀x(Fx→Ff(x))">∀x(∃y(Fy ∧ x=f(y)) → Fx) ↔ ∀x(Fx → Ff(x))</a></li>
<li class="formula"><a href="#□(p→q)→□p→□q">□(p→q) → □p→□q</a></li>
<li class="formula"><a href="#∀x□Fx→□∀xFx">∀x□Fx → □∀xFx</a></li>
<li class="formula"><a href="#∀y∃xFxy→∃x∀yFxy">∀y∃xFxy → ∃x∀yFxy</a></li>
<li class="formula"><a href="#p∨q,¬p|=q">p∨q, ¬p |= q</a></li>
</ul>
<h3>Entering formulas</h3>
<p>To enter logic symbols, use the buttons above the text field, or
type
<span class="formula">~</span> for <span class="formula">¬</span>,
<span class="formula">&</span> for <span class="formula">∧</span>,
<span class="formula">v</span> for <span class="formula">∨</span>,
<span class="formula">-></span> for <span class="formula">→</span>,
<span class="formula"><-></span> for <span class="formula">↔</span>,
<span class="formula">!</span> for <span class="formula">∀</span>,
<span class="formula">?</span> for <span class="formula">∃</span>,
<span class="formula">[]</span> for <span class="formula">□</span>,
<span class="formula"><></span> for <span class="formula">◇</span>. You can
also use LaTeX commands.</p>
<h3>Premises</h3>
<p>If you want to test an argument with premises and conclusion,
use <span class="formula">|=</span> to separate the premises from the
conclusion, and use commas to separate the premises. See the last example in
the list above.</p>
<h3>Syntax of formulas</h3>
<p>Any alphabetic character is allowed as a propositional constant, predicate,
individual constant, or variable. Numeral digits can be used either as
singular terms or as "subscripts" (but don't mix the two uses). '+', '*',
and '-' can be used as function expressions. Predicates (except identity)
and function terms must be in prefix notation. Function terms must have
their arguments enclosed in brackets. So
<span class="formula">F2x17</span>, <span class="formula">Rab</span>,
<span class="formula">R(a,b)</span>, <span class="formula">Raf(b)</span>,
<span class="formula">F(+(1,2))</span> are ok, but
not <span class="formula">Animal(Fred)</span>, <span class="formula">aRb</span>,
or <span class="formula">F(1+2)</span>. (In fact, these are also ok, but
they won't be parsed as you might expect.) The order of precedence among
connectives is <span class="formula">¬, ∧, ∨, →, ↔</span>. Association is to
the right. Quantifier symbols in sequences of quantifiers must not be
omitted: write <span class="formula">∀x∀yRxy</span> instead
of <span class="formula">∀xyRxy</span>.</p>
<h3>Supported logics</h3>
<p>Besides classical propositional logic and first-order predicate logic (with
functions and identity), a few normal modal logics are supported. If you
enter a modal formula, you will see a choice of how the accessibility
relation should be constrained. For modal predicate logic, constant domains
and rigid terms are assumed.</p>
<h3>Source code</h3>
<p>The source is <a href="https://www.github.com/wo/tpg">on github</a>.</p>
<h3>Contact</h3>
<p>Comments, bug reports and suggestions are always welcome:
<script language="javascript">
document.write(("<a href='mailto:wo%umsu.de'>wo%umsu.de</a>.").replace(/%/g, '@'));
</script>
</p>
</div>
</div>
</body>
</html>