diff options
author | Jed Barber <jjbarber@y7mail.com> | 2014-04-08 15:06:40 +1000 |
---|---|---|
committer | Jed Barber <jjbarber@y7mail.com> | 2014-04-08 15:06:40 +1000 |
commit | 03d38eb3190eb5e51fb18847fe0792013285bde5 (patch) | |
tree | 1060d26d3042b5c0c5b1c027fac45fe87f3d685a /readme.txt | |
parent | f2c4e4614613ede497f19ef79dc7dc157eaca834 (diff) |
Reorganising source code
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. + + |