QF_NRAにゼロ除算が含まれていますか？

Question

ゼロ除算はQF_NRAに含まれていますか？

この問題では、SMT-LIB標準が混乱しています。 paper where the standard is definedでは、この点については説明しません。実際、NRAとQF_NRAはその文書のどこにも表示されません。いくつかの情報はstandard websiteで提供されています。実数は次のように定義されます。

- all terms of the form (/ m n) or (/ (- m) n) where 
    - m is a numeral other than 0, 
    - n is a numeral other than 0 and 1, 
    - as integers, m and n have no common factors besides 1. 

これは、定数値に関しては、分母からゼロを明示的に除外します。しかし、後に、分割は次のように定義されます

-/as a total function that coincides with the real division function 
    for all inputs x and y where y is non-zero, 

これはノートによって追跡されます。最初の引用符は(/ m 0)がQV_NRA内の数字ではないことを言うので

Since in SMT-LIB logic all function symbols are interpreted as total 
    functions, terms of the form (/ t 0) *are* meaningful in every 
    instance of Reals. However, the declaration imposes no constraints 
    on their value. This means in particular that 
    - for every instance theory T and 
    - for every closed terms t1 and t2 of sort Real, 
    there is a model of T that satisfies (= t1 (/ t2 0)). 

これは、一見矛盾しています後者の言葉では、/はt1とt2のいずれに対しても(= t1 (/ t2 0))が充足できるという関数であることを示しています。

事実上の現実は、(/ m n)がnが0でない場合の唯一の実数であるにもかかわらず、0による除算がSMT-LIBに含まれるように見えることです。これは、私の前の質問に関連している：最初の引用は（/ M 0）と述べているy=1/x, x=0 satisfiable in the reals?

Answer 1

ありません数

ではありませんが、それはそれが何であるかを数言いません。

は後者の引用は/（= T1（/ T 2 0））は、任意のT1およびT2

これが正しいのために充足可能であるような関数であることを言います。

「ゼロ除算は許可されていません！」という学校の考え方から離れる必要があります。これは未定義です。 Undefinedは、これがどのような値であるかを指定する公理がないことを意味します。 （これは学校でも同様です）

f(1234)とは何ですか？定義されていないので、Z3は何の番号も選択できません。 a/0とf(a)の間に違いはありません。fは何らかの解釈されていない機能です。 Z3は好きな機能を埋め込むことができます。

したがって、a/0 == bは充足可能であり、aとbはすべてOKです。しかし、(a/0) == (a/0) + 1はfalseです。

数学演算子は単なる関数です。規格は、これらの機能を部分的に指定している。