---
title: "Set Variables"
authors:
  - "W. W. Bledsoe"
doi: ""
url: "https://ijcai.org/proceedings/1977/116"
pdf: "https://ijcai.org/proceedings/1977/0116.pdf"
venue: "Proceedings of the Fifth International Joint Conference on Artificial Intelligence"
year: 1977
pages: "501-509"
track: "Theorem Proving"
keywords:
---

# Set Variables

W. W. Bledsoe

*Proceedings of the Fifth International Joint Conference on Artificial Intelligence*, pages 501-509.

## 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.