It was during my first months in my PhD when it wasn't clear what I will do. My idea was to define the theorems as operators of planning algorithms and then to

It was during my first months in my PhD when it wasn't clear what I will do. My idea was to define the theorems as operators of planning algorithms and then to use the planning techniques to create new theorems or probes. But planning is not good for long plans as theorem proving, so we moved to something simpler: linear equations and A* algorithm. Then we found the math equations have different representations for the same thing and the branch factor is quite big. Moreover the heuristic of trying to minimize the equations doesn't give good results some times. That is why the prototype works for the example, but for other examples the a* gets lost in the search because of branch factor and equation representation. The problem with the equation representation is that if you don't find a good one, then you cannot make searches in hash tables efficiently. You end up with a lot of equations duplicated with different representations. And the representation, I used trees for it, was important for the operators. Planning was a very nice idea because the algorithms already deal with the heuristics. But algorithms as FF http://www.cs.toronto.edu/~sheila/2542/s14/A1/hoffmannebel-FF-jair01.pdf http://www.cs.toronto.edu/~sheila/2542/s14/A1/hoffmannebel-F... wouldn't work due to the branch factor and the relaxation of the problem it performs.