Heavy-Tailed Behavior and Randomization in Proof Planning

摘要: Proof Planning planning considers mathematical theorems as problems. A proof problem is defined by an initial state specified the assumptions, goal given theorem to be proved, and a set of operators called methods. Finding corresponds therefore searching for sequence that derive from assumptions. In system MEGA (Benzmuelleret al. 1997) traditional approach enriched incorporating knowledge into process (see (Melis & Siekmann 1999) details). particular, methods represent mathematically meaningful inference steps can specific domain. We explore domain residue classes over integers ((Meier, Pollet, Sorge 2000)) using approach. apply solve large testbeds algebraic problems class (e.g. ) together with binary operation such closed respect , associative etc. The results these proofs are in turn used classify structure terms it forms, i.e., whether semi-group, monoid Moreover, another classification divides structures equivalence isomorphic structures. During this we have prove obligations stating two or not. Our experiments show hardest instances correspond not (non-isomorphism problems). For some planner generates long proofs, run times, while other (similar) short times. Since able find heuristic rule enables us control unpredictability planner’s performance, randomization restart techniques boost search increase solvability horizon non-isomorphism