---
title: "Equality Elimination for the Inverse Method and Extension Procedures"
authors:
  - "Anatoli Degtyarev"
  - "Andrei Voronkov"
doi: ""
url: "https://ijcai.org/proceedings/1995/45"
pdf: "https://ijcai.org/proceedings/1995/0045.pdf"
venue: "Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence"
year: 1995
pages: "342-346"
track: "Automated Reasoning"
keywords:
---

# Equality Elimination for the Inverse Method and Extension Procedures

Anatoli Degtyarev, Andrei Voronkov

*Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence*, pages 342-346.

## 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. Solution clauses are obtained by a very refined strategy - basic superposition with selection function. In the second part, we perform the usual sequent proof search by the inverse method. Our approach is called equality elimination because we eliminate all occurrences of equality in the first part of the proof. Unlike the previous approach proposed by Maslov, our method uses most general substitutions, ordering restrictions and selection functions. We also note that this technique is directly applicable to extension procedures, like the connection method. Unlike other approaches, we do not require the use of rigid or mixed Eunification.