[isabelle-dev] Experiments in best-first-search rewriter

[Bohua Zhan]

Hi, Tobias

Thanks for the reply. My main motivation here is to try to write
something that more closely resembles how humans think. I understand
this is very far from being able to be included in the main
repository. This is just to explore different approaches.

In particular I would be interested in test cases that are simple for
a human (so we may expect the computer to solve it during proof
development), but difficult for a BFS rewriter like this, because they
may show some heuristics that humans use, that perhaps can be
incorporated into an automated prover.

Best,
Bohua