Equality Reasoning in Clause Graphics

Abstract

A method to control the application of equalityderivation rules in an automatic theorem proving system is presented . When handling eq uality in the search for a pro o f of a theorem two main problems arise: 1) to obtain a control mechanism for the s ea r ch 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 t e rms unifiable. Thes e pr ob lems are solved by combining th e c laus e graph method and the "paramodulation-if-needed" idea by introducing Morris' E-resolution into th e clause graph proof procedure. The n eces sary equations to form possible E-resolvents are searched for in th e initial graph and are inh e rited afterwards. Th e search space f o r possible E -resolutions will be r ed uced by exploiting constraints using th e information in the clause graph.