When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic

Zachary Kincaid, Nicolas Koh, Shaowei Zhu

This paper presents a theory of non-linear integer/real arithmetic and algorithms for reasoning about this theory. The theory can be conceived as an extension of linear integer/rea…