Equality Elimination for the Inverse Method and Extension Procedures

Abstract

We demonstrate how to handle equality in the inverse method using equality elimination. In the equality elimination method, proofs consist of two parts. In the first part we try to solve equations obtaining so called solution clauses. In the second part, we perform the usual sequent proof search by the inverse method. Our method is called equality elimination because we eliminate all occurrences of equality in the first part of the proof. Solution clauses are obtained by using a very strong strategy -- basic superposition. Unlike the previous approach proposed by Maslov, we prove completeness of our method with most general substitutions and with ordering restrictions. We also note that these technique can be adapted to extension procedures, like the connection method. Unlike other approaches, we do not require the use of rigid or mixed E-unification.