Optimizing Backward Chaining Resolution Tableau Theorem Provers
Explore the goal of optimizing performance in backward chaining resolution tableau theorem provers through subgoal ordering. Understanding the significance of subgoal ordering decisions and the research gap in this area. Comparing similar work on subgoal alternation in model elimination and detailing the planned system involving first-order formulas, subgoal sequencing, and proof loops. Delve into the proof of concept regarding subgoal permutations' impact on performance and the collection of data at subgoal selection points.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Ordering Subgoals in a Backward Chaining Prover KERT SZ GERG PAPP GERG SZEREDI P TER VARGA D NIEL ZOMBORI ZSOLT
The what What is the goal of the project? The optimization of the performance of backward chaining resolution tableau theorem provers by subgoal ordering.
To get on the same page Backward-chaining Starts from the statement to be proved Builds a proof-tree (tableau) Leafs are subgoals to be proven Used system LeanCoP Uses first order formulas The method should work for every backward-chaining system Used languages Prolog Python
and the why Why subgoal ordering? Two important decisions in the proving process What inference to use In what order to use the subgoals Less research has been done
Similar work Subgoal Alternation in Model Elimination Ibens, Letz Difference We try to order the subgoals at a choice point, while this work is mainly about changing subgoal branches before a proof branch is complete
Planned system First order formula Context & subgoal set Advisor ML system LeanCoP prover Subgoal sequence Proof
Planned system First order formula FoF to Inner Proof loop Subgoal set & context Advisor ML system Subgoal selection Subgoal sequence Proof loop Create proof
Proof of concept Data Gathering First order formula How do different permutations of subgoals effect performance? FoF to DNF Chosen metric: Number of inferences Proof loop On the basic setting leanCoP chose the first subgoal In data gathering mode, we try all possible permutations Subgoal selection Subgoal permutation Proof loop Create readable proof
Proof of concept Collected data At one subgoal selection point, we collected the following tuples: <S,C, , (C),I> S - Set of clauses in the goal C - Current set of subgoals - A permutation (C) - C permuted according to I - the number of inferences it takes to get a proof for (C) Two rules for optimization and to avoid redundancy: Omit redundant permutations T Time limit on branches after D depth.
Proof of concept - Heuristics Based on the collected data we observed the following three general rules. Negated goals before positives Equality predicates with variables on both side last Other equality predicates first
Proof of concept First order formula We ran the modified leanCoP proof process on the M2k dataset in 4 ways: FoF to DNF Original order Proof loop Reversed order Random order Heuristic guided selection Heuristic guided order Metric\Ordering Proven theorems in 1 second Average inferences* Heuristic 824 Original 712 Random 707 Reversed 783 Proof loop 2938 3103 3041 2388 Create readable proof
Advisor Input data Q(f(a,b), s(b)) Enigma vector The encoded context Q Creation s f Take the abstract syntax tree Take an n long path on the tree ( n {1,2,3} ) b a b Count its occurances The k. element of the vector is the occurances of the k. path. The vector is hashed The vector is sparse so key collision is rare Train data Created by running the data gathering phase
Advisor Variable set size There is no theoretical upper bound for the number of subgoals Most architectures can t handle this Solutions Make the model learn and evaluate pairwise comparisons Map the model to a vector/matrix of a given size Evaluate the input into a score Choose the permutation with the smallest score Use a model that can handle variable set size
Conclusions and further work Proof of concept shows promising results Unfortunately the advisor system is not properly fine tuned for the problem due to time-constraints. Further work Refining the advisor model Try different models For example set-to-sequence transformers.
