Applications

We will demonstrate an application of reflection to the task of adding sound decision procedures to tactic-oriented provers. For the sake of illustration, we take a very simple and familiar example -- the decision problem for classical tautologies. A more realistic example would be decision procedures commonly used such as arith or $sup\!-\!in\!f$, but those are too complex to treat in these lectures, and the tautology procedure is used in some provers, see [18].