2. Intuition of how grind works🔗

All descriptions of grind tell you to imagine that grind works with a "virtual whiteboard". First grind writes all the hypotheses and the goal on the whiteboard. All proofs that grind produces are by contradiction, so it negates the goal and doesn't further distinguish it from the hypotheses.

Afterwards, grind uses several different engines to find a proof, i.e. discover a contradiction. To ensure that these engines can work together, they all put discovered facts back on the whiteboard, so that another engine may use them.

This document is supposed to be a short introduction on how to use grind in your projects. So we will only discuss parts that especially relevant to either a basic understanding of grind or to its usage.