Thanks 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

Thanks 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!