Nonlinear Arithmetic with SMTLIB Division is Undecidable
计算机科学中的逻辑
2026-05-27 v1
摘要
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.
引用
@article{arxiv.2605.26181,
title = {Nonlinear Arithmetic with SMTLIB Division is Undecidable},
author = {Dejan Jovanovic},
journal= {arXiv preprint arXiv:2605.26181},
year = {2026}
}