ASSIP-T: A Theorem-Proving Machine

Abstract

An associative processor for theorem provi ng in first order logic is described. It i s designed on the basis of the deduction plan method, introduced by Cox and Pietrzykowski. The main features of this method are the Separation of unifi cation fro m deduction and the incorporation of a meth o d for intelligent backtracking. This kind of backtracking is based on a special unification procedure. An improved version of thi s unification procedure is given, which ou tputs a unification graph with constrai nts. In the case of a unification conf lict, sufficient information for a directed backtracking step can be gained from the unification graph . According to the deduction plan method, the ASSIP-T memory consists of two parts, one for the deduction plan and the other for the unif i cat i o n graph. ASSIP-T can perform deduction and unification in parallel. Both memory parts consist of a set 6f subparts eac h of which keeps the information about cla use s or terms , respectively. A subpart is a lin ear array of cells provided with a contro l unit and can be regarded as a subprocesso r.