A Completion-Based Method for Mixed Universal and Rigid E-Unification

We present a completion-based method for handling a new version of E-unification, called "mixed" E-unification, that is a combination of the classical "universal" E-unification and "rigid" E-unification. Rigid E-unification is an important method for handling equality in Gentzen-type first-order calculi, such as free-variable semantic tableaux or matings. The performance of provers using E-unification can be increased considerably, if mixed E-unification is used instead of the purely rigid version. We state soundness and completeness results, and describe experiments with an implementation of our method.

• Type: Conference
• Year: 1994
• Where: CADE
• Authors: Bernhard Beckert
• Keywords: CADE 1994, Completion-based Method, Free-variable Semantic Tableaux, Gentzen-type First-order Calculi, Logical Reasoning