3 ms·

Some years ago I tried to do something a bit more complex: http://telauges.appspot.com/mathsolver/ http://telauges.appspot.com/mathsolver/ My idea was to use p

by jorgemf 10y ago

Some years ago I tried to do something a bit more complex: http://telauges.appspot.com/mathsolver/ http://telauges.appspot.com/mathsolver/ My idea was to use planning and A* search to solve any type of math problem, even create probes for things like the quadratic equation https://en.wikipedia.org/wiki/Quadratic_equation https://en.wikipedia.org/wiki/Quadratic_equation . I gave up after learnt the search space was so big for it that it was impossible to solve. If I had to do it today I will explore deep learning as heuristic, but I think it probably wont work. I always like to see this type of projects, I hope they succeed where I failed.

jahewson 10y ago
Perhaps that was an over-ambitious project given that Automated Theorem Proving is an entire field of research. https://en.m.wikipedia.org/wiki/Automated_theorem_proving https://en.m.wikipedia.org/wiki/Automated_theorem_proving
- jorgemf 10y ago
  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.

by jorgemf 10y ago

jahewson 10y ago

Perhaps that was an over-ambitious project given that Automated Theorem Proving is an entire field of research. https://en.m.wikipedia.org/wiki/Automated_theorem_proving https://en.m.wikipedia.org/wiki/Automated_theorem_proving

jorgemf 10y ago
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.