I understand your decision problem as follows: we are given finitely many real constants and a formula $F$ that is a disjunction of linear inequalities in the form you mention, having real variables $x_i$, using the specified real constants and having some unspecified integer parameters $p_i$. This instance of the decision problem is to decide yes-or-no given that data whether that formula with those real constants admit some assignment of the integer parameters making the formula universally true for all reals $x_i$. If this is the decision problem that you meant (and please correct me if I have misunderstood), then it is not decidable. The reason is that we cannot even decide whether two real numbers $c$ and $d$ are equal (imagine giving a "yes" answer after finitely many steps of computation, which can inspect only finitely much of $c$ and $d$; one could change the reals in an uninspected part). It follows that, similarly, the question $c\leq d$ for real numbers is undecidable. But the question of $c\leq d$ is equivalent to the validity of the system $F=$ $(x\geq c)\vee(x\leq d)$' in your system, which can be expressed as $(x\geq c)\vee(-x\geq -d)$. So your decision problem is not decidable, even for instances having no integer parameters. This argument actually shows that the decision problem of your system is not even semi-decidable, for if we could get the yes answers for validity in your system, then we could recognize positive instances of $c\leq d$, and we can already recognize instances of $d\lt c$, since any such inequality is revealed by a finite stage of inspecting $c$ and $d$, if given for example as Cauchy sequences with known convergence. Thus, by combining the two algorithms, we would be able to decide $c\leq d$, which we cannot. Since your decision problem involves real constants, it would make sense to analyze it with some of the other infinitary notions of computability, such as [Blum-Shub-Smale model](http://en.wikipedia.org/wiki/Blum%E2%80%93Shub%E2%80%93Smale_machine), where equality of reals is decidable. And for the BSS model, I'm not sure how it comes out.