---
title: "ASSIP-T: A Theorem-Proving Machine"
authors:
  - "Werner Dilger"
  - "Hans-Albert Schneider"
doi: ""
url: "https://ijcai.org/proceedings/1985/242"
pdf: "https://ijcai.org/proceedings/1985/0242.pdf"
venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence"
year: 1985
pages: "1194-1199"
track: "Theorem Proving"
keywords:
---

# ASSIP-T: A Theorem-Proving Machine

Werner Dilger, Hans-Albert Schneider

*Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 1194-1199.

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