Rigid E-unification is the problem of unifying two expressions modulo a set
of equations, with the assumption that every variable denotes
exactly one term (rigid semantics). This form of unification
was originally developed as an approach to integrate equational
reasoning in tableau-like proof procedures, and studied extensively
in the late 80s and 90s. However, the fact that
simultaneous rigid E-unification is undecidable has limited
practical adoption, and to the best of our knowledge there is no
tableau-based theorem prover that uses rigid E-unification. We introduce
simultaneous bounded rigid E-unification (BREU), a new version of rigid
E-unification that is bounded in the sense that variables only represent
terms from finite domains. We show that (simultaneous) BREU is
NP-complete, outline how
BREU problems can be encoded as propositional SAT-problems, and use
BREU to introduce a sound and complete sequent calculus for
first-order logic with equality.