Proceedings

Equality Elimination for the Inverse Method and Extension Procedures

Anatoli Degtyarev, Andrei Voronkov

Download BibTeX Cite

Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. 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.

Anatoli Degtyarev, and Andrei Voronkov. 1995. Equality Elimination for the Inverse Method and Extension Procedures. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI-95. IJCAI, 342–346. https://ijcai.org/proceedings/1995/45
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards