We present an E-unification procedure for a set of non-ground (dis)equations, along with a dynamic set of ground (dis)equations, and prove its completeness. The ground part is dynamic in the sense that it continually changes. The algorithm saturates the non-ground equations using Superposition modulo the ground theory. We also have an Instantiation rule that matches the left hand side of non-ground (dis)equations with ground terms, creating new ground (dis)equations, which changes the ground theory. This algorithm can be used in quantified SMT problems, where the dynamic ground theory represents the evolving model. We develop an ordering to compare terms modulo a ground theory, which is used to orient non-ground equations. We prove properties of this ordering, using a weak form of monotonicity and subterm property. We finally present a set of inference rules for our ordering, which allows us to properly orient equations in theories of some finite data structures, such as a theory of finite lists with length and append.

翻译：我们提出了一种针对一组非基(不)等式与动态基(不)等式的E-消解过程，并证明了其完备性。其中基部分具有动态性，会持续变化。该算法利用基理论上的超归结方法对非基等式进行饱和处理。我们还引入了一个实例化规则，使非基(不)等式的左侧与基项匹配，生成新的基(不)等式，从而改变基理论。该算法可应用于量化的SMT问题，其中动态基理论代表不断演化的模型。我们开发了一种基于基理论比较项的公理化序，用于对非基等式进行定向。我们证明了该序的弱单调性和子项性质。最后，我们为这种序给出了一组推理规则，使其能够正确地对某些有限数据结构理论（如带有长度和追加运算的有限列表理论）中的等式进行定向。