-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
135 lines (121 loc) · 4.68 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
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>Visualisation of prrofs with tableaux</title>
<meta name="GENERATOR" content="Quanta Plus">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<h1>Visualisation for the Tableau calculus</h1>
<p>The Tableau Calculus is a formal method to prove statements in First Order Predicate Logic.
It is explained in extenso for instance in the
<a href="">scriptum to the lecture formal methods (German)</a>.</p>
<h2>Using the applet</h2>
<p>A new proof can be started using the <img src="classes/de/uka/ilkd/tablet/img/new.gif">-Button.
You will be asked to enter one or more formulas spearated by ';'.
See <A href="#formGram">description below</A> on
how to enter formulas.
</p>
<p>Nodes in the proof are color-coded according to their "type" of formula:</p>
<table cellpadding="5">
<tbody>
<tr>
<td bgcolor="#80ff80" width=50></td>
<td><b>ALPHA</b></td>
<td>Non-branching formulas with subformulas (such as A ∧ B)</td>
</tr>
<tr>
<td bgcolor="#8080ff"></td>
<td><b>BETA</b></td>
<td>Branching formulas with subformulas (such as A ∨ B)</td>
</tr>
<tr>
<td bgcolor="#80ffff"></td>
<td><b>GAMMA</b></td>
<td>Universally quantified formula (∀x. A(x))</td>
</tr>
<tr>
<td bgcolor="#ffff80"></td>
<td><b>DELTA</b></td>
<td>Existentially quantified formula (∃x. A(x))</td>
</tr>
<tr>
<td bgcolor="#ff80ff"></td>
<td><b>NEGNEG</b></td>
<td>Special case: Double negation (¬¬A), resolves to A</td>
</tr>
</tbody>
</table>
<p>You can drag a formula holding your <strong>left</strong> mouse button (formula becomes
<em>red</em>) onto a leaf of the tree to apply the according rule to this branch. The leaf
must not be closed. If you want to expand a formula on the spot, you can click on it twice.
You can also drag a formula with your <strong>right</strong> mouse button pressed (formula
becomes <em>green</em>) onto a contradictory formula (i.e. A onto ¬ A or v.v.) to close
branches.</p>
<p>The application of gamma rules create new free variables called
<code>X<em>n</em></code> with n a natural number.
These free variables can be instantiated using the
<img src="classes/de/uka/ilkd/tablet/img/instance.gif">-button. A message box pops up and you
can enter the instantiation for one free variable in the form
<code>X<em>n</em> = <em>formula</em></code>.
</p>
<p>You can undo rule applications and instantiations using the
<img src="classes/de/uka/ilkd/tablet/img/undo.gif">-button. Please note that closed branches
may become reopend hereby.
</p>
<APPLET code="de.uka.ilkd.tablet.TableauApplet" codebase="classes" align="baseline"
width="700" height="700"/>
<p>If the formulas are not clearly visible or if you prefer ASCII rather than mathematical
formulas, you can switch between ASCII and Unicode characters using the
<img src="classes/de/uka/ilkd/tablet/img/unicode.gif">-button.
</p>
<h2>On the notation of formulas</h2>
<p>
The grammar for formulas is straight forward and will be presented here by examples.
Identifiers can be any character string (case sensitive!) starting with a letter (optionally)
followed by letters or digits. You must not use <code>X1, X2, ...</code> and
<code>sk1, sk2, ...</code> however, for these are reserved for free variables and
skolem symbols respectively. </p>
<table>
<tbody>
<tr>
<td><code>A x. p(x)</code></td>
<td>for all x, p(x) holds. p is a predicate here.</td>
</tr>
<tr>
<td><code>E x. p(f(x))</code></td>
<td>There is a x so that p(f(x)) holds. p is a predicate and f is a function here</td>
</tr>
<tr>
<td><code>P & Q</code></td>
<td>P and Q hold.</td>
</tr>
<tr>
<td><code>P -> Q</code></td>
<td>P implies Q</td>
</tr>
<tr>
<td><code>P | Q</code></td>
<td>P or Q</td>
</tr>
<tr>
<td><code>P | Q & R</code></td>
<td>Operators have the usual precedence: & then | then ->. I.e.
<code>P | Q & R = P | (Q & R)</code>
</td>
</tr>
<tr>
<td><code>A x. p(x) | q(x)</code></td>
<td><strong>Caution!</strong> This is equal to <code>(A x. p(x)) | q(x)</code>.
Therefore x appears as free variable which may not be. The applet does not check for such
things, so be aware!
</td>
</tr>
<tr>
<td></td>
<td></td>
</tr>
</tbody>
</table>
</body>
</html>