Heavy-Tailed Behavior and Randomization in Proof Planning
Andreas Meier, Carla Pedro Gomes, Erica Melis⋆ · 2001
.36> ; +) such as RSn is closed with respect to ffi, RSn is associative with respect to ffi etc. The results of these proofs are in turn used to classify a given structure (RSn ; ffi) in terms of the algebraic structure it forms, i.e., whether it is a semi-group, monoid etc. Moreover, another classification process divides given residue class structures into equivalence classes of isomorphic structures. During this classification process we have to prove proof obligations stating that two structures are isomorphic or not. Our experiments show that the hardest problem instances correspond to problems stating that two structures are not isomorphic (non-isomorphism problems). For some instances the planner generates long proofs, with long run times, while for other (similar) instances the planner generates sh