A short introduction to the grind tactic

4. Basic derivations of new facts🔗

First we will consider the basic ways that grind uses to derive new facts. With "basic" I mean that it neither uses any lemmas nor specialized solvers. We will not go into too much detail here because this part of grind doesn't provide too much interactivity for the user.

  1. 4.1. Congruence closure
  2. 4.2. Constraint Propagation
  3. 4.3. Case Splits