tpg/index.php at master · wo/tpg · GitHub

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
<!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>

<!--
I want this page to work even if PHP is not supported. To this end,
we're inside a HTML comment here that hides the PHP code from the browser.
The comment is closed immediately below if php is supported.
<?php
echo '--'.'>';
$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";
}
// Need to re-open the HTML comment:
echo '<!'.'--';
/*
We're inside both a HTML and a PHP comment here. If PHP is supported,
everything up to the closing C-style comment marker is ignored. If
PHP is unsupported, the following HTML is rendered by the browser.
-->
<script src='array.js'></script>
<script src='formula.js'></script>
<script src='parser.js'></script>
<script src='prover.js'></script>
<script src='equality.js'></script>
<script src='modelfinder.js'></script>
<script src='sentree.js'></script>
<script src='painter.js'></script>
<script src='index.js'></script>
<script src='index.js'></script>
<script>
function log(args) {}
</script>
<!--
Now we're back inside both a HTML and a PHP comment.
*/ ?>
-->

<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">-&gt;</span> for <span class="formula">→</span>,
    <span class="formula">&lt;-&gt;</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 indices (as in <span class="formula">Fx1</span>), 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>