diff options
Diffstat (limited to 'readme.txt')
-rw-r--r-- | readme.txt | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/readme.txt b/readme.txt new file mode 100644 index 0000000..9a55603 --- /dev/null +++ b/readme.txt @@ -0,0 +1,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. + + |