linear rational theory

The complete theory of the rational numbers (with addition and multiplication) is undecidable, since it can encode the property of being a natural number.

The theory of linear arithmetic over the rationals $T_Q$ is decidable in a more efficient way than the corresponding theory in the integers.

（带量词和无量词的片段都可判定）

signature是$V_Q=\{0,1,+,-,=,\ge \}$

常数有整数就够了。有理数的系数不是必要的，因为可以通过乘公倍数把（不）等式变为整系数的。