-
Notifications
You must be signed in to change notification settings - Fork 4
/
help.html
48 lines (29 loc) · 1.06 KB
/
help.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
<html lang="fr">
<head>
<script id="MathJax-script" async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
<link href="engine.css" rel="stylesheet">
<script src="js/main.js"></script>
<meta charset="UTF-8">
</head>
<body>
<h1>Help</h1>
Proofs are represented by so-called tree proofs. Each node is of the form:
<br/>
<proof>
<proofs>
<proof>
<infer>Premisse 1</infer>
</proof>
<proof>
<infer>Premisse 2</infer>
</proof>
</proofs>
<infer>Conclusion</infer>
</proof>
This is read: "From premisse 1 and premisse 2, I prove the conclusion".
<h2>Why this tool?</h2>
Tired with proofs written in text?
Tired of searching Equation 4 and Lemma 5.3.2 when you read "Equation (4) and Lemma 5.3.2 leads to...".
The advantage here is that the premisses used to prove a conclusion are graphically near.
</body>
</html>