Ist die Division durch Null in QF_NRA enthalten?

Question

Ist die Division durch Null in QF_NRA enthalten?

Der SMT-LIB-Standard ist in dieser Angelegenheit verwirrend. Die paper where the standard is defined diskutiert einfach diesen Punkt nicht, tatsächlich erscheinen NRA und QF_NRA nirgendwo in diesem Dokument. Einige Informationen finden Sie unter standard website. Reals sind definiert als einschließlich:

- 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. 

Dies schließt explizit Null aus dem Nenner, wenn es zu konstanten Werten kommt. Doch später wird Teilung wie folgt definiert:

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

Dies wird durch eine Notiz weiterverfolgt:

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)). 

Dies ist scheinbar widersprüchlich, weil das erste Zitat sagt, dass (/ m 0) ist keine Zahl in QV_NRA, aber das letztere Zitat sagt, dass / eine Funktion ist, so dass (= t1 (/ t2 0)) für alle t1 und t2 erfüllbar ist.

Die De-facto-Realität auf dem Boden ist, dass Division durch Null scheint in SMT-LIB enthalten sein, trotz der Aussage, dass (/ m n) ist nur eine echte Zahl, wenn n ist nicht Null. Dies wird auf eine frühere Anfrage von mir bezogen werden: y=1/x, x=0 satisfiable in the reals?

Answer 1

das erste Zitat sagt, dass (/ m 0) ist keine Zahl

Nein, aber es sagt nicht, welche Zahl es ist.

aber letztere Zitat sagt, dass/eine Funktion, so dass (= t1 (/ T2 0)) für jeden t1 erfüllbar ist und t2

Das ist richtig.

Sie müssen weg von der Schule Mentalität, die sagt "Division durch Null ist nicht erlaubt!". Es ist undefiniert. Undefiniert bedeutet, dass es kein Axiom gibt, das angibt, um welche Werte es sich handelt. (Und das gilt auch für die Schule.)

Was ist f(1234)? Es ist undefiniert, also darf Z3 irgendeine Nummer wählen. Es gibt keinen Unterschied zwischen a/0 und f(a), wobei f eine nicht interpretierte Funktion ist. Z3 kann jede beliebige Funktion ausfüllen.

Daher ist a/0 == b erfüllbar und alle a und b sind in Ordnung. Aber (a/0) == (a/0) + 1 ist falsch.

Mathematische Operatoren sind nur Funktionen. Der Standard spezifiziert diese Funktionen teilweise.