Nonlinear Arithmetic with SMTLIB Division is Undecidable
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914601993502720 |
|---|---|
| author | Jovanovic, Dejan |
| author_facet | Jovanovic, Dejan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_26181 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Nonlinear Arithmetic with SMTLIB Division is Undecidable Jovanovic, Dejan Logic in Computer Science 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. |
| title | Nonlinear Arithmetic with SMTLIB Division is Undecidable |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.26181 |