An extension of the inverse method to the predicate calculus with equality

A modification of the inverse method of establishing deducibility is proposed. The aim of this modification is to improve the processing with equalities. Some strategies are analysed and some possibilities of refinement are investigated.