4 ms·
I thought I understood your problem statement as something along the lines of "How do I stop the rule (a+b)->(b+a) from firing just because they can". So my pr
by jdmichal 6y ago
I thought I understood your problem statement as something along the lines of "How do I stop the rule (a+b)->(b+a) from firing just because they can". So my proposal was to only attempt to apply certain rules if they helped reach the goal, where the goal was simplification. They would not fire in and of themselves, but always in a chain that ended in some desired simplification rule also firing.
- hyperpallium2 6y agoThanks for explaining. I want the user in manual control, and the problem is how the user specifies what is to be done. I did entertain some automation as one way to achieve this: to present a set of different things that could be done - and the user could select from that set, instead of specifying the details explicitly. It's not my preferred approach, because it suggest/hints more to the user than I want to ... but it is a solution to the specification problem. I think I can see your suggestion as a refinement of that approach, of not blindly listing every possible next step, but just the most useful ones. And further, selecting from a set of different series of rule applications. One could also rank them. Your version of the problem is appropriate for a proof assistent - but I'm aiming at something quite a bit more rudimentary! ---- BTW my motivation for this project is partly to get clear on some formal aspects of proof - the mathematics I've studied so far has only formalized some domains, but not proof itself. I can also feel it as a fun game, to be able to transform expressions... though whether that turns out to be the case remains to be seen!