Automated reasoning with real numbers I have a large number of equivalences which look like:
$(a \leq 0.54 \wedge b \geq 0.12) \vee (c \gt 0.98)$ $\Leftrightarrow$ $(x \leq 0.25) \vee (x \gt 0.91 \wedge y \geq 0.01)$
This is just an example. In general, formulae on either left or right side of the equivalence  could be anything that takes the form of a disjunctive normal form (DNF) clause, the numbers could be any real numbers with a fixed precision, and the inequality signs could be $\leq$, $\lt$, $\geq$, or $\gt$.
What is important is that the possible variables on the left side of all the formulae (here $\{a, b, c\}$) form a set that is distinct from the possible variables on the right side of all the formulae (here $\{x, y, z\}$). There could be any fixed number of variables on either side: doesn't need to be 3 variables, and doesn't need to be an equal number on either side.
I also have some implications of the form:
$(a \leq 0.32 \wedge b \geq 0.62)$ $\Rightarrow$ $(c \gt 0.00)$
Here both left and right sides are just conjunctions of inequalities, but what is important is that the set of variables on both left and right sides, i.e. $\{a, b, c\}$ here, is the same as the set of variables on only the left side of the previous kind of the formula (i.e. the equivalences).
My question is: what kind of automated reasoner would I need to find the logical consequences of a set of such formulae? I am just looking for a concrete identification of the general class of problems this belongs to, and any out-of-the-box reasoners which may be available. Perhaps this is an SMT problem?
In your case, the simplest solution may be to use SAT.
Your first clause includes $x \le 0.25$ and $x &gt; 0.91$. This means that there are five regions of interest for the variable $x$, which we identify with boolean variables: $X_1 \equiv x \in(-\infty, 0.25)$, $X_2 \equiv x = 0.25$, $X_3 \equiv x \in (0.25, 0.91)$, $X_4 \equiv x = 0.91$, $X_5 \equiv x \in (0.91,\infty)$.
Create a boolean variable for each of these ranges, and convert the clause to use them. So, for example, $x \le 0.25$ would convert to $X_1 \vee X_2$, and $x &lt; 0.91$ would convert to $X_1 \vee X_2 \vee X_3$.
More clauses would mean more constants, and hence more ranges of interest for a primitive variable.