Set Variables

Abstract

A procedure is described that gives values to set variables in automatic theorem proving. The result is that a theorem is thereby reduced to first order logic, which is often much easier to prove . This procedure handles a part of higher order logic, a small but important part. It is not as general as the methods of Huet, Andrews, Pietrzykowski, and Haynes and Henschen, but it seems to be much faster when it applies. It is more in the spirit of J . L. Darlington's FMatching. This procedure is not domain specific: results have been obtained in intermediate analysis (the intermediate value theorem), topology, logic, and program verification (finding internal assertions). This method is a "maximal method" in that a largest (or maximal) set is usually produced if there is one. A preliminary version has been programmed for the computer and run to prove several theorems.