SMT-LIB の QF_NRA ロジックは決定可能ですか?
Tarski が、実数の多項式系が決定可能であるという意味で、非線形算術が決定可能であることを証明したことを知っています。ただし、QF_NRA には分割が含まれているため、QF_NRA がこの傘に該当するかどうかは明らかではありません。したがって、最初の問題は、QF_NRA の除算に、分母がゼロになる可能性がある変数による除算が含まれているかどうかです。 別の質問として投稿しました。これに答えるのは、それだけでは十分に難しいことが判明したためです。
ゼロによる除算が QF_NRA の一部でない場合、QF_NRA の除算は乗算に変換でき、Tarski によって証明されているように、問題は決定可能になります。除算が実際に QF_NRA に含まれている場合は、確信が持てません。私の感じでは、ゼロによる除算が発生する場合に導入された新しい変数を使用して、問題をケースごとに分割することができます。この場合、QF_NRA は依然として決定可能です。