The loss of faith in the grand scheme for problem solving has lately been matched by a loss of faith in any grand scheme for theorem proving. (This should come as no surprise--the tasks differ only slightly.) The limitations of brute force and very simple heuristics are now clear enough that other approaches to producing practically useful theorem provers have been appearing for some time now. De Champeaux’s paper presents an approach one might describe as “distributed,” and he goes so far as to suggest some of the pieces out of which a reasonable theorem prover might be built.

De Champeaux argues that theorem proving will be done best by a committee of “cooperating deductive specialists,” each being called upon at the appropriate moment, insofar as that can be determined. The specialties in question might be things like finding a new point of view or finding a generalization of the problem to be solved. Other members of the committee will surely be the traditional diggers, for example, an expert on resolution and perhaps one on natural deduction.

The main discussion in the paper concerns two candidates for jobs on the team, one called INSTANCE and one called INSURER. The former has the task of determining whether a formula being inspected is a special case of another, in particular of something already accepted as known. The latter decomposes proof tasks into collections of presumably simpler such tasks. These two specialists are discussed in detail, and examples of how they can work together are given. Experiments comparing their joint work favorably with that of simpler approaches are supplied.

It is really too early in the development of this subject to know what tools will be considered useful in the future. The direction outlined in this paper is encouraging and deserves exploration. The paper concludes with a short discussion of who else might serve on the envisioned committee, and I hope future papers will report on happy experiences with welcoming these newcomers aboard.