99 setup Sledgehammer_Fact_Preprocessor.setup |
99 setup Sledgehammer_Fact_Preprocessor.setup |
100 use "Tools/Sledgehammer/sledgehammer_hol_clause.ML" |
100 use "Tools/Sledgehammer/sledgehammer_hol_clause.ML" |
101 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" |
101 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" |
102 setup Sledgehammer_Proof_Reconstruct.setup |
102 setup Sledgehammer_Proof_Reconstruct.setup |
103 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" |
103 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" |
104 |
104 use "Tools/ATP_Manager/atp_manager.ML" |
105 use "Tools/ATP_Manager/atp_wrapper.ML" |
105 use "Tools/ATP_Manager/atp_wrapper.ML" |
106 setup ATP_Wrapper.setup |
106 setup ATP_Wrapper.setup |
107 use "Tools/ATP_Manager/atp_manager.ML" |
|
108 use "Tools/ATP_Manager/atp_minimal.ML" |
107 use "Tools/ATP_Manager/atp_minimal.ML" |
109 |
|
110 text {* basic provers *} |
|
111 setup {* ATP_Manager.add_prover ATP_Wrapper.spass *} |
|
112 setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *} |
|
113 setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *} |
|
114 |
|
115 text {* provers with stuctured output *} |
|
116 setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *} |
|
117 setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *} |
|
118 |
|
119 text {* on some problems better results *} |
|
120 setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *} |
|
121 |
|
122 text {* remote provers via SystemOnTPTP *} |
|
123 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *} |
|
124 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *} |
|
125 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *} |
|
126 |
|
127 use "Tools/Sledgehammer/sledgehammer_isar.ML" |
108 use "Tools/Sledgehammer/sledgehammer_isar.ML" |
128 |
109 |
129 |
110 |
130 subsection {* The MESON prover *} |
111 subsection {* The MESON prover *} |
131 |
112 |