Towards an advanced implementation of the connection method
Wolfgang Bibel, Elmar Eder, Bertram Fronhoefer · International Joint Conference on Artificial Intelligence · 1983
This paper is intended to give a glance at some issues involved in implementing an advanced proof component based on the connection method. The material presented comprises contributions to the following problem domains: (a) Dealing with formulas In non-normal form, (b) The dynamic incorporation of unification into a proof procedure, (c) Controlling the generation of copies of clauses.