summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

changeset 55597 | 25d7b485df81 |

parent 55596 | 928b9f677165 |

child 56220 | 4c43a2881b25 |

1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Wed Feb 19 15:57:02 2014 +0000 1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Wed Feb 19 15:57:02 2014 +0000 1.3 @@ -3,6 +3,42 @@ 1.4 1.5 Proof reconstruction for Leo-II. 1.6 1.7 +USAGE: 1.8 +* Simple call the "reconstruct_leo2" function. 1.9 +* For more advanced use, you could use the component functions used in 1.10 + "reconstruct_leo2" -- see TPTP_Proof_Reconstruction_Test.thy for 1.11 + examples of this. 1.12 + 1.13 +This file contains definitions describing how to interpret LEO-II's 1.14 +calculus in Isabelle/HOL, as well as more general proof-handling 1.15 +functions. The definitions in this file serve to build an intermediate 1.16 +proof script which is then evaluated into a tactic -- both these steps 1.17 +are independent of LEO-II, and are defined in the TPTP_Reconstruct SML 1.18 +module. 1.19 + 1.20 +CONFIG: 1.21 +The following attributes are mainly useful for debugging: 1.22 + tptp_unexceptional_reconstruction | 1.23 + unexceptional_reconstruction |-- when these are true, a low-level exception 1.24 + is allowed to float to the top (instead of 1.25 + triggering a higher-level exception, or 1.26 + simply indicating that the reconstruction failed). 1.27 + tptp_max_term_size --- fail of a term exceeds this size. "0" is taken 1.28 + to mean infinity. 1.29 + tptp_informative_failure | 1.30 + informative_failure |-- produce more output during reconstruction. 1.31 + tptp_trace_reconstruction | 1.32 + 1.33 +There are also two attributes, independent of the code here, that 1.34 +influence the success of reconstruction: blast_depth_limit and 1.35 +unify_search_bound. These are documented in their respective modules, 1.36 +but in summary, if unify_search_bound is increased then we can 1.37 +handle larger terms (at the cost of performance), since the unification 1.38 +engine takes longer to give up the search; blast_depth_limit is 1.39 +a limit on proof search performed by Blast. Blast is used for 1.40 +the limited proof search that needs to be done to interpret 1.41 +instances of LEO-II's inference rules. 1.42 + 1.43 TODO: 1.44 use RemoveRedundantQuantifications instead of the ad hoc use of 1.45 remove_redundant_quantification_in_lit and remove_redundant_quantification 1.46 @@ -2189,7 +2225,11 @@ 1.47 end 1.48 *} 1.49 1.50 + 1.51 +section "Importing proofs and reconstructing theorems" 1.52 + 1.53 ML {* 1.54 +(*Preprocessing carried out on a LEO-II proof.*) 1.55 fun leo2_on_load (pannot : TPTP_Reconstruct.proof_annotation) thy = 1.56 let 1.57 val ctxt = Proof_Context.init_global thy 1.58 @@ -2220,4 +2260,28 @@ 1.59 end 1.60 *} 1.61 1.62 +ML {* 1.63 +(*Imports and reconstructs a LEO-II proof.*) 1.64 +fun reconstruct_leo2 path thy = 1.65 + let 1.66 + val prob_file = Path.base path 1.67 + val dir = Path.dir path 1.68 + val thy' = TPTP_Reconstruct.import_thm true [dir, prob_file] path leo2_on_load thy 1.69 + val ctxt = 1.70 + Context.Theory thy' 1.71 + |> Context.proof_of 1.72 + val prob_name = 1.73 + Path.implode prob_file 1.74 + |> TPTP_Problem_Name.parse_problem_name 1.75 + val theorem = 1.76 + TPTP_Reconstruct.reconstruct ctxt 1.77 + (TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference) 1.78 + prob_name 1.79 + in 1.80 + (*NOTE we could return the theorem value alone, since 1.81 + users could get the thy value from the thm value.*) 1.82 + (thy', theorem) 1.83 + end 1.84 +*} 1.85 + 1.86 end 1.87 \ No newline at end of file