Heavy-Tailed Behavior and Randomization in Proof Planning

Model-Based Validation of Intelligence

Volume

Papers from the 2001 AAAI Spring Symposium

Contents

Our experiments show the effectiveness of our randomized proof planning approach by showing a significant improvement in performance over a testbed of 160 non-isomorphism problems. In particular, with our approach, a much larger fraction of problem instances is solvable (from 67.5% to 97.5%; 2hr time limit per proof) and a variety of proofs is generated for each problem instance. Our work demonstrates that randomization and restarts can be successfully applied to deduction systems. We believe these results are very promising and might apply to other problem domains using deduction techniques such as e.g., software verification.