blob: 9a55603677b812d80aadff0d1f601d2a34e4137c (
plain)
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
|
Semantic <input file>
Evaluates a proof trace, and shows the contents of the Dictionary, Assumptions, Stack and Theorems when done.
Syntactic <input file>
Checks a proof trace for syntax errors.
ProofGraph <input file>
Constructs a DAG dependency graph of the virtual machine commands used in a given proof trace.
WriteProof <input file> > <output file>
Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it back into a linear proof trace.
Delete <input file> [<num#1>, <num#2>, <num3>] > <output file>
Removes all theorems of specified numbers from a proof trace. Best used in conjunction with ListThm, so you can
actually know what theorems are what. Generates a simplified proof trace as output.
Concat <input #1> <input#2> <input #2> > <output file>
Joins two proof traces together, converts it to a DAG and back again, then outputs the result.
ListThm <input file>
Displays numbered theorems from a proof trace. Best used in conjunction with Delete so you know what theorems you
are deleting.
|
