summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | sultana |

Wed, 19 Feb 2014 15:57:02 +0000 | |

changeset 55597 | 25d7b485df81 |

parent 55596 | 928b9f677165 |

child 55598 | da35747597bd |

child 55611 | 8ae36527c2a6 |

added a function that carries out all the reconstruction steps, for improved usability;
added documentation;

src/HOL/TPTP/TPTP_Proof_Reconstruction.thy | file | annotate | diff | comparison | revisions | |

src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Wed Feb 19 15:57:02 2014 +0000 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Wed Feb 19 15:57:02 2014 +0000 @@ -3,6 +3,42 @@ Proof reconstruction for Leo-II. +USAGE: +* Simple call the "reconstruct_leo2" function. +* For more advanced use, you could use the component functions used in + "reconstruct_leo2" -- see TPTP_Proof_Reconstruction_Test.thy for + examples of this. + +This file contains definitions describing how to interpret LEO-II's +calculus in Isabelle/HOL, as well as more general proof-handling +functions. The definitions in this file serve to build an intermediate +proof script which is then evaluated into a tactic -- both these steps +are independent of LEO-II, and are defined in the TPTP_Reconstruct SML +module. + +CONFIG: +The following attributes are mainly useful for debugging: + tptp_unexceptional_reconstruction | + unexceptional_reconstruction |-- when these are true, a low-level exception + is allowed to float to the top (instead of + triggering a higher-level exception, or + simply indicating that the reconstruction failed). + tptp_max_term_size --- fail of a term exceeds this size. "0" is taken + to mean infinity. + tptp_informative_failure | + informative_failure |-- produce more output during reconstruction. + tptp_trace_reconstruction | + +There are also two attributes, independent of the code here, that +influence the success of reconstruction: blast_depth_limit and +unify_search_bound. These are documented in their respective modules, +but in summary, if unify_search_bound is increased then we can +handle larger terms (at the cost of performance), since the unification +engine takes longer to give up the search; blast_depth_limit is +a limit on proof search performed by Blast. Blast is used for +the limited proof search that needs to be done to interpret +instances of LEO-II's inference rules. + TODO: use RemoveRedundantQuantifications instead of the ad hoc use of remove_redundant_quantification_in_lit and remove_redundant_quantification @@ -2189,7 +2225,11 @@ end *} + +section "Importing proofs and reconstructing theorems" + ML {* +(*Preprocessing carried out on a LEO-II proof.*) fun leo2_on_load (pannot : TPTP_Reconstruct.proof_annotation) thy = let val ctxt = Proof_Context.init_global thy @@ -2220,4 +2260,28 @@ end *} +ML {* +(*Imports and reconstructs a LEO-II proof.*) +fun reconstruct_leo2 path thy = + let + val prob_file = Path.base path + val dir = Path.dir path + val thy' = TPTP_Reconstruct.import_thm true [dir, prob_file] path leo2_on_load thy + val ctxt = + Context.Theory thy' + |> Context.proof_of + val prob_name = + Path.implode prob_file + |> TPTP_Problem_Name.parse_problem_name + val theorem = + TPTP_Reconstruct.reconstruct ctxt + (TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference) + prob_name + in + (*NOTE we could return the theorem value alone, since + users could get the thy value from the thm value.*) + (thy', theorem) + end +*} + end \ No newline at end of file

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Wed Feb 19 15:57:02 2014 +0000 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Wed Feb 19 15:57:02 2014 +0000 @@ -6,12 +6,30 @@ NOTE - Makes use of the PolyML structure. - looks for THF proofs in the path indicated by $THF_PROOFS + - these proofs are generated using LEO-II with the following + configuration choices: -po 1 -nux -nuc --expand_extuni + You can simply filter LEO-II's output using the filter_proof + script which is distributed with LEO-II. *) theory TPTP_Proof_Reconstruction_Test imports TPTP_Test TPTP_Proof_Reconstruction begin +section "Main function" +text "This function wraps all the reconstruction-related functions. Simply + point it at a THF proof produced by LEO-II (using the configuration described + above), and it will try to reconstruct it into an Isabelle/HOL theorem. + It also returns the theory (into which the axioms and definitions used in the + proof have been imported), but note that you can get the theory value from + the theorem value." + +ML {* + reconstruct_leo2 (Path.explode "$THF_PROOFS/NUM667^1.p.out") @{theory} +*} + +section "Prep for testing the component functions" + declare [[ tptp_trace_reconstruction = false, tptp_test_all = false,