Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem (Q1960430)

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 aims at presenting results in this area and filling in proofs of some results that have been announced but 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.