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.