3.4.6 Reasoners

Reasoners are applied to the sequent of a given proof tree node and provide a way to contribute to the provers. They are typically of more interest to the developer than the user.

A reasoner is (and has to be) quite “rough" : it takes a given sequent and produces a proof rule that will (if possible) apply to this given sequent. A tactic can use several reasoners by applying them in loops, combining them, or even calling other tactics.