the next generation of the in-browser educational proof assistant
Create README.md
authored by
Liam O'Connor
and committed by
GitHub
00657eca
6e189db3
+63
+63
README.md
+63
README.md
···
1
+
## Holbert NG
2
+
3
+
This is a new, from-scratch development of my [reconceived design](https://liamoc.net/forest/loc-000V) of the Holbert proof assistant -- the browser based Higher Order Logic proof assistant.
4
+
5
+
Rather than a standalone web-app, Holbert NG will be a library of web components that can be seamlessly integrated into online documents.
6
+
I envision it working like this, for HTML documents:
7
+
8
+
Index.html:
9
+
```html
10
+
<html>
11
+
<head>
12
+
<script src="holbert.mjs" type="module" />
13
+
<script type="module">
14
+
Holbert.setup({
15
+
termLanguage: FirstOrderTerms, //also planned: HigherOrderTerms, Strings
16
+
components: [GrammarDefinition, FunctionDefinition] // examples of extra components provided by planned plugins
17
+
methods: [CalculationalProof, HoareDerivation] // examples of extra proof methods provided by planned plugins.
18
+
})
19
+
</script>
20
+
</head>
21
+
<body>
22
+
<hol-config id="index.html/displaysettings">
23
+
{ rules: "Gentzen" }
24
+
</hol-config>
25
+
<p>Lets introduce the rules for conjunction:</p>
26
+
<hol-rules id="index.html/andRules" deps="index.html/displaysettings">
27
+
A.B.
28
+
A B
29
+
-------- andI
30
+
(/\ A B)
31
+
A.B.
32
+
(/\ A B)
33
+
-------- andE1
34
+
A
35
+
36
+
A.B.
37
+
(/\ A B)
38
+
-------- andE2
39
+
B
40
+
</hol-rules>
41
+
<p>Proving commutativity of conjunction:</p>
42
+
<hol-proof id="index.html/andComm" deps="index.html/displaysettings index.html/andRules">
43
+
forall A B.
44
+
assuming *: (/\ B A)
45
+
shows (/\ A B)
46
+
by andI(A B) {
47
+
- by andE2(A B) {
48
+
- by *
49
+
}
50
+
- by andE1(A B) {
51
+
- by *
52
+
}
53
+
}
54
+
</hol-proof>
55
+
</body>
56
+
</html>
57
+
```
58
+
59
+
Note that the ids of each block are prefixed with a file name. These documents can span multiple HTML pages and any other dependencies are automatically fetched.
60
+
Modifications are automatically saved to local storage.
61
+
In addition, the entire language of Holbert NG is representable both textually and graphically.
62
+
63
+
I plan to develop a small plug-in to make these components easily integratable into [Forester](https://www.forester-notes.org) documents as well.