Heavy-Tailed Behavior and Randomization in Proof Planning

Andreas Meier, Carla Gomes, and Erica Melis

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.