We show that the nonlinear real arithmetic theory (NRA) as defined in the SMTLIB standard is undecidable. The undecidability arises from the treatment of division by zero as an uninterpreted function, which allows encoding integer arithmetic problems into NRA formulas.

翻译：我们证明SMTLIB标准中定义的非线性实数算术理论（NRA）是不可判定的。该不可判定性源于将除以零视为未解释函数的处理方式，这使得整数算术问题能被编码为NRA公式。