SMT-LIB의 QF_NRA 로직이 결정 가능합니까?

Question

SMT-LIB의 QF_NRA 로직이 결정 가능합니까?

나는 타르 스키가 실수로 다항식의 시스템을 결정할 수 있다는 비선형 산수를 결정할 수 있다는 것을 증명했습니다. 그러나 QF_NRA에는 부서가 포함되어 있기 때문에 QF_NRA가이 우산 아래 있다는 것은 명백하지 않습니다. 따라서 첫 번째 질문은 QF_NRA의 분할이 분모가 잠재적으로 0 인 변수에 의한 나누기를 포함하는지 여부입니다. I posted that as a separate question인데, 이는 답변 자체가 모두 충분하지 않기 때문입니다.

0으로 나눈 값이 QF_NRA의 일부가 아닌 경우 QF_NRA의 나누기를 곱하기로 변환 할 수 있으며 문제는 Tarski가 증명 한대로 결정할 수 있습니다. 실제로 사업부가 QF_NRA에 포함된다면 나는 확신하지 못합니다. 제 생각에 문제는 여전히 0으로 나누는 경우에 새로운 변수가 도입되어 사례별로 분해 될 수 있습니다. 이 경우 QF_NRA는 여전히 결정할 수 있습니다.

Answer 1

결정할 수 있습니다.

당신은이 문제에 나타나는 각 (/ T1의 T2)에 대한 즉 필요한 곳을 axiomatize 해석의 기능으로 부서를 처리하여 SMT-LIB 사업부를 인코딩 할 수 있습니다, 당신은 효과

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

이를 추가 할 수 있습니다 QF_NRA의 SMT-LIB 이론을 실재 (나눗셈없이)와 해석되지 않은 함수의 두 이론의 조합으로 축소합니다. 이제는 실수와 해석되지 않은 함수가 양자 한정어가 아닌 조각의 결정할 수있는 이론이므로 Nelson과 Oppen의 고전적 논증에 의존하여 결합 이론을 결정할 수 있음을 보여줄 수 있습니다.

Yices2은 예를 들어 MCSAT에 근거한 실제와 해석되지 않은 기능의 조합을 결정할 수 있습니다. Z3은 내가 아는 한 실제와 해석되지 않은 기능을 결합 할 수 없으며 CVC4에는 아직 실제에 대한 결정 절차가 없습니다.