Update README.md

data61 · Feb 12, 2018 · 2246506 · 2246506
1 parent 207146b
commit 2246506
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/PaMpeR/README.md b/PaMpeR/README.md
@@ -21,8 +21,10 @@
 ## Contents
 - **PaMpeR.thy**: The main theory file of PaMpeR. Users can install PaMpeR by importing this theory file into their own theory file.
 - **Assertions.ML**: This file contains 60 assertions we developed to extract feature values from proof states.
-- **method_names**: This file contains the list of proof method names appearing our target proof corpora, Isabelle's standard library. If users optimize PaMpeR based on their own proof corpora, this list will be updated.
-- Note that the following four sub-directories are useful only for those people who want to optimize PaMpeR or those who want to reproduce our preliminary evaluation of PaMpeR.
+- **method_names**: This file contains the list of proof method names appearing in our target proof corpora, Isabelle's standard library. If users optimize PaMpeR based on their own proof corpora, this list will be updated.
+- **regression_trees.txt**: This file contains the results of our regression tree algorithm. This file is the outcome of **Build_Regression_Tree** session, but one can use this file as the default learning results to avoid the time consuming operation of database extraction.
+- Note that the following files and sub-directories are useful only for those people who want to optimize PaMpeR or those who want to reproduce our preliminary evaluation of PaMpeR.
+   - **outer_syntax.ML**: The standard distribution of Isabelle forbits us from over-writing the deinition of Isabelle keywords. We have to disable this feature to over-write the definition of the **apply** command and the **by** command for database extraction and evaluation by replacing **Isabelle/src/Pure/Isar/outer_syntax.ML** with this file. 
    - **Build_Database**: This Isabelle session extracts feature vectors from proof corpora and build a file called Database in PSL/PaMpeR/Build_Database.
    - **Preprocess**: This Isabelle session converts the raw database produced by Build_Database to a group of databases and store these databases in PSL/PaMpeR/Databases. Each database in PSL/PaMpeR/Databases corresponds to a proof method used in the training data. This transformation converts our multi-output regression problem to a group of single-output regression problem.
    - **Build_Regression_Tree**: This Isabelle session takes the databases in PSL/PaMpeR/Databases and analyse them to produce regression trees for each proof method.