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
|
# Chadprover
## Overview
An automated theorem-prover for propositional logic. This will be updated for first-order logic. The prover is exposed as an API using the Dream web framework.
Steps:
1. Lex the raw input (a string representing the formula to prove) to generate a list of tokens.
2. Parse the token list to generate a syntax tree.
3. Check validity? (expensive operation)
4. Run sequent calculus computation on the negation of the formula.
5. Return list of sequents that prove the formula.
## Lexing
We first lex the input, obtaining the following possible tokens:
```
type tok =
| TRUE
| FALSE
| LIT of string
| NOT
| AND
| OR
| IMPLIES
| IFF
| LEFT_PAREN
| RIGHT_PAREN
| SKIP
```
## Parsing
First, we decided on an appropriate grammar for parsing the token list.
### Approach 1: Naive Grammar
#### Simple CFG
```
S ::= E $
E ::= TRUE
| FALSE
| LIT s
| NOT E
| E AND E
| E OR E
| E IMPLIES E
| E IFF E
| LEFT_PAREN E RIGHT_PAREN
```
#### Issues
- we need to encode precedence
- above grammar is ambiguous
- consider `NOT E OR E`, which can be parenthesized as `(NOT E) OR E` vs. `NOT (E OR E)`
### Approach 2: LL(1) Grammar
#### CFG redefined as LL(1) grammar
```
S ::= E $
E ::= F E'
E' ::= IFF F E' | eps
F ::= G F'
F' ::= IMPLIES G F' | eps
G ::= H G'
G' ::= OR H G' | eps
H ::= I H'
H' ::= AND I H' | eps
I ::= NOT I | LEFT_PAREN E RIGHT_PAREN | TRUE | FALSE | LIT s
```
#### FIRST Sets
```
FIRST(S) = FIRST(E)
= FIRST(F)
= FIRST(G)
= FIRST(H)
= FIRST(I)
= {TRUE, FALSE, LIT s, NOT, LEFT_PAREN}
FIRST(E') = {IFF, eps}
FIRST(F') = {IMPLIES, eps}
FIRST(G') = {OR, eps}
FIRST(H') = {AND, eps}
```
#### FOLLOW Sets
```
FOLLOW(E) = {$, RIGHT_PAREN}
FOLLOW(E') = FOLLOW(E) = {$, RIGHT_PAREN}
FOLLOW(F) = FIRST(E') U FOLLOW(E') U FOLLOW(E) = {IFF, $, RIGHT_PAREN}
FOLLOW(F') = FOLLOW(F) = {IFF, $, RIGHT_PAREN}
FOLLOW(G) = FIRST(F') U FOLLOW(F') U FOLLOW(F) = {IMPLIES, IFF, $, RIGHT_PAREN}
FOLLOW(G') = FOLLOW(G) = {IMPLIES, IFF, $, RIGHT_PAREN}
FOLLOW(H) = FIRST(G') U FOLLOW(G') U FOLLOW(G) = {OR, IMPLIES, IFF, $, RIGHT_PAREN}
FOLLOW(H') = FOLLOW(H) = {OR, IMPLIES, IFF, $, RIGHT_PAREN}
FOLLOW(I) = FIRST(H') U FOLLOW(H') U FOLLOW(H) = {AND, OR, IMPLIES, IFF, $, RIGHT_PAREN}
```
#### Notes
- this approach can work, but the grammar is quite convoluted
- LL parsers are relatively straightforward to implement, however, so we opt for this approach (for now)
### Approach 3: LR Grammar
#### LR(1) Grammar
```
S ::= E $
E ::= E IFF F | F
F ::= F IMPLIES G | G
G ::= G OR H | H
H ::= H AND I | I
I ::= NOT I | LEFT_PAREN E RIGHT_PAREN | TRUE | FALSE | LIT s
```
#### FIRST Sets
```
FIRST(S) = FIRST(E)
= FIRST(F)
= FIRST(G)
= FIRST(H)
= FIRST(I)
= {TRUE, FALSE, LIT s, NOT, LEFT_PAREN}
```
#### FOLLOW Sets
```
TODO
```
#### Notes
- this is probably the best approach with the simplest grammar
- we might switch to an LR parser in the future
## Useful Commands
- `dune build` to build the project
- `dune test` to run tests
- `dune exec chadprover` to execute the program
## Project Log
### Dune Setup
- `dune init proj chadprover` to create project directory (we rename the base dir as *Chadprover*)
- `dune build` to build the project
- `dune test` to run tests
- `dune exec chadprover` to execute the program
### Dream Setup
- `opam install dream`
- add *dream* to libraries in */bin/dune*: `(libraries chadprover dream)`
- add *dream* to package dependencies in */dune-project*: ` (depends ocaml dune dream)`
- add Lwt preprocessing to */bin/dune*: `(preprocess (pps lwt_ppx))`
- this tells dune to preprocess the code with an AST rewriter that can transform Lwt promises (e.g. `let%lwt = ...`)
- same with `ppx_yojson_conv` (Jane Street's library that converts between JSON and OCaml data types)
### Issues
- avoid giving a file the same name as its directory; Dune treats both files and directories as modules, so it can't distinguish between them if they have the same name
## To Do
### Short-Term
- input sanitizer (no inputs longer than set number of vars, no $ signs)
- use OCaml modules
- get API up and running
- read into Lwt library
### Ideas
- brute force solver
- prolog solver
- sequent calculus solver (with intermediate steps)
- tableau calculus
- free variable tableau calculus
- propositional and first-order logic
- other L&P parts?
- Hoare logic?
### Fixes
- none for now
## Resources
- https://dune.readthedocs.io/en/latest/quick-start.html
- https://ocaml.org/docs/compiling-ocaml-projects
- https://aantron.github.io/dream/
|
