EUFⁿ：带未解释函数的等式理论的可判定扩展
EUF$^n$: A Decidable Extension to the Theory of Equality with Uninterpreted Functions
浏览论文内容
中文总结 AI 辅助
本研究提出带参数化组合深度的EUFⁿ理论，通过条件同余图算法证明其可判定性，可用于解决交错Dyck可达性及未解释程序验证的相关问题。
中文摘要 AI 辅助
带未解释函数的等式理论（EUF）是约束求解和程序验证的基础，未解释函数可抽象具体实现，实现定理与证明的泛化和简化。但标准EUF将函数组合限制为固定有限深度（如fᵏ(x)，其中k为常数）。本研究将EUF扩展为EUFⁿ，支持一元函数的参数化组合深度（如fⁿ(x)，其中n为自然数变量）。EUFⁿ公式可视为无限多个EUF公式的析取，每个EUF公式由自然数赋值实例化，其可满足性定义为至少一个此类实例化EUF公式的可满足性。我们通过条件同余图（CCG）算法证明EUFⁿ可满足性问题的可判定性，该算法通过维护项之间的条件等价关系，将标准同余闭包过程泛化，将可满足性问题归约为带可除性的Presburger算术中存在性语句的判定，该问题可判定，从而得到EUFⁿ无量词片段的判定过程，其复杂度上界为2NEXPTIME。EUFⁿ增强的表达力支持新应用：（1）编码交错Dyck可达性问题的可判定子类，现有过/欠近似会产生假正例/假负例；（2）编码未解释程序验证问题的新可判定子类。
英文摘要
The theory of Equality with Uninterpreted Functions (EUF) is fundamental to constraint solving and program verification. Uninterpreted functions abstract concrete implementations, enabling generalization and simplification of theorems and proofs. However, standard EUF restricts function composition to fixed finite depths (\emph{e.g.}, $f^k(x)$ where $k$ is constant). This work extends EUF to EUF$^n$, supporting \emph{parametric composition depth} for unary functions (\emph{e.g.}, $f^n(x)$ where $n$ is a natural number variable). An EUF$^n$ formula can be viewed as a disjunction of infinitely many EUF formulas, each instantiated by an assignment of natural numbers. Its satisfiability is defined by the satisfiability of at least one such instantiated EUF formula. We establish the decidability of the EUF$^n$ satisfiability problem via a \emph{conditional congruence graph (CCG)} algorithm. This approach generalizes the standard congruence closure procedure by maintaining conditional equivalence relations between terms. The algorithm reduces the satisfiability problem to deciding existential sentences in Presburger arithmetic with divisibility, which is a decidable problem, thereby yielding a decision procedure for the quantifier-free fragment of EUF$^n$ with a 2NEXPTIME complexity upper bound. The enhanced expressiveness of EUF$^n$ enables new applications: (1) Encoding a decidable subclass of interleaved Dyck reachability problems where existing over/under-approximations produce false positives/negatives, and (2) Encoding a new decidable subclass of uninterpreted program verification problems.
