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 | |
parent | f2c4e4614613ede497f19ef79dc7dc157eaca834 (diff) |
Reorganising source code
Diffstat (limited to 'README')
-rw-r--r-- | README | 51 |
1 files changed, 0 insertions, 51 deletions
@@ -1,51 +0,0 @@ - - -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. - - |