Fix automation

Question

Fix automation

Closed this issue 7 years ago · 2 comments

We need to fix auto soon; @cangiuli and I believe strongly that this should be our principle priority at this time, and it needs to happen before we write much more RedPRL code, and before we can really start recommending that people try RedPRL.

A big source of frustration with auto is the small-step nature of it; in order to implement the needed proof search tactics, we need a ton of backtracking (which can be avoided in a big-step version). Instead, we should engineer things so that problems are posed in the order that they can be solved, and that they are solved in one big step, modulo emitting subgoals that require user intervention.

Related is #438; I open this as a separate ticket because I want to track the task of fixing auto regardless of the specificities of that proposal.

Answer 1 · 2018-02-09T21:36:37.000Z

What exactly needs to be fixed now?

Answer 2 · 2018-02-09T21:38:14.000Z

I think it’s better than it was, but the main problem remains that it is a little unpredictable, often loops, and we don’t really understand how to study the proof search scientifically.

…

On Feb 9, 2018, at 4:36 PM, favonia ***@***.***> wrote: What exactly needs to be fixed now? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.