2

Is the QF_NRA logic in SMT-LIB decidable?

I know that Tarski proved that nonlinear arithmetic is decidable, in the sense that systems of polynomials in the real numbers are decidable. However, it's not obvious that QF_NRA falls under this umbrella, because QF_NRA contains division. So the first question is whether or not division in QF_NRA includes division by variables where the denominator is potentially zero. I posted that as a separate question, because answering that turns out to be difficult enough all on its own.

If division by zero is not part of QF_NRA, then division in QF_NRA can be converted to multiplication, and the problem will be decidable as proven by Tarski. If division is in fact included in QF_NRA, then I'm less sure. My feeling is that the problem can still be broken up case-wise, with new variables introduced for the cases where division by zero occurs. In this case QF_NRA would still be decidable.

Douglas B. Staple
  • 10,510
  • 8
  • 31
  • 58

1 Answers1

4

It is decidable.

You can encode SMT-LIB division by treating division as an uninterpreted function that you axiomatize where needed, i.e. for each (/ t1 t2) appearing in the problem, you can add 

t2 != 0 => t1 = (/ t1 t2)*t2  .

This in effect reduces the SMT-LIB theory of QF_NRA to the combination of two theories: reals (without division) and uninterpreted functions. Now, since both reals and uninterpreted functions are decidable theories in the quantifier-free fragment, you can rely on the classic arguments of Nelson and Oppen to show that the combination theory is decidable.

Yices2, for example, can decide such combinations of reals and uninterpreted functions (based on MCSAT). Z3, as far as I know, can not combine reals and uninterpreted functions, and CVC4 does not yet have a decision procedure for the reals.

Dejan Jovanović
  • 2,085
  • 1
  • 16
  • 22
  • Isn't that axiomatization equivalent to just using `/` directly? – usr Oct 22 '16 at 11:49
  • Thank you, your proposal for theory combination is a formalization of what I was imagining regarding handling the `t2 == 0` case separately from the `t2 != 0` case, the latter permitting the division to be eliminated, and the former being solvable in its own right, by introducing a new symbol for `(/ t1 t2)`. – Douglas B. Staple Oct 23 '16 at 17:12