---
title: "A Definition-Driven Theorem Prover"
authors:
  - "George W. Ernst"
doi: ""
url: "https://ijcai.org/proceedings/1973/8"
pdf: "https://ijcai.org/proceedings/1973/0008.pdf"
venue: "Proceedings of the Third International Joint Conference on Artificial Intelligence"
year: 1973
pages: "51-54"
track: "Theorem Proving and Logic: 1"
keywords:
---

# A Definition-Driven Theorem Prover

George W. Ernst

*Proceedings of the Third International Joint Conference on Artificial Intelligence*, pages 51-54.

## Abstract

This paper describes a theorem prover, running on a PDP-10-TENEX system, that can prove some theorems whose statements involve a relatively large number of definitions. Such theorems require special methods because (1) their statements contain a large number of clauses and (2) their proofs are quite long although straight-forward. A theorem is proven by first subdividing it into "simple" subgoals and then using a standard resolution theorem prover to prove the subgoals. The first part of this process involves the substitution of definitions for defined quantities and the use of logical simplification. This process which is more similar to a natural deduction system than a resolution system, is shown to be complete when restricted to first-order logic. However, the theorem prover can deal with some interesting higher-order theorems as is shown by an example.