PII: S0304-3975(98)00317-X Theoretical ELSEVIER Computer Science Theoretical Computer Science 224 ( 1999) 3 19-352 www.elsevier.com/locateitcs Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem Andrei Voronkov* Uppsalu University, Computing Sciencr Department, Box 311, S-75105 Uppsuh. Swwkn Abstract Recently, a number of results have been published related to simultaneous rigid E-unification and Herbrand’s theorem for logic with equality. The aim of this article is to overview these results, fill in some proofs that have only been sketched before, and present some new results. @ 1999 Elsevier Science B.V. All rights reserved. 1. Introduction Herbrand’s theorem is one of the major tools in automated deduction in classical logic. The tableau method, the connection method and model elimination are based on a direct use of this theorem. Variants of Herbrand’s theorem are used in completeness proofs for nearly all methods of automated deduction, including variants of resolution. Recently, a number of results about Herbrand’s theorem and proof search for logic with equality have been published. This article aim at presenting results in this area and filling in proofs of some results that have been announced by not formally justified. We also give more precise formulations of results with respect to the signatures in which problems are formulated and provide a table of known results. 2. Preliminaries The equality predicate is denoted z=. The symbol t- denotes provability in classical logic. By [XI H tl, . . . ,x, H t,] we denote the substitution that replaces variables xi by terms t;. If 0 is a substitution and t is a term, then to denotes the term obtained from t by applying 0. An expression (e.g. a term or a set of terms) is called ground if it contains no variables. * Fax: +46 18 5 11530; e-mail: [email protected] 0304-3975/99/$-see front matter @ 1999 Elsevier Science B.V.