Equality reasoning in clause graphs
Karl-Hans Bläsius · International Joint Conference on Artificial Intelligence · 1983
A method to control the application of equality derivation rules in an automatic theorem proving system is presented. When handling equality in the search for a proof of a theorem two main problems arise: 1) to obtain a control mechanism for the search and application of useful equality derivation steps in order to support global strategies which plan and control the whole proof, thus conducing to an efficient and complete proof procedure. 2) to find proper equations rendering two terms unifiable. These problems are solved by combining the clause graph method and the Mparamodulation-if-needed idea by introducing Morris' E-resolution into the clause graph proof procedure. The necessary equations to form possible E-resolvents are searched for in the initial graph and are inherited afterwards. The search space for possible E-resolutions will be reduced by exploiting constraints using the information in the clause graph.