In theorem proving, it may be possible to use a * model* of the
theorem to be proved to prune the search space.

H. Gelernter[H. Gelernter, ``Realization of a Geometry-Theorem
Proving Machine'', in E. A. Feigenbaum and J. Feldman, * Computers
and Thought*, McGraw-Hill, 1963, pp. 134-152.]
used a diagram of a geometry theorem as a filter.
If a subgoal to be proved is true in the diagram, that may be just
a coincidence. However, if a subgoal is false in the diagram, it
cannot be part of any general theorem; thus, the subgoal can be
failed at once.