Begrenzung universell quantifizierte Variable

Question

Ich würde gerne wissen, ob es möglich ist, den Bereich der Werte einer universell quantifizierten Variablen in Z3 zu begrenzen.

Nehmen wir zum Beispiel an, dass ich eine Variable vom Typ Real namens "Zeit" habe, die verwendet wird, um die Zeit im System zu modellieren. Nehmen wir an, ich habe eine Behauptung, die besagt, dass der Wert einer unären Funktion "func1" immer zwischen 1 und 100 liegen soll. Die Funktion nimmt die Eingabe als Zeitvariable. Ausgedrückt in Z3, ich habe die Eigenschaft wie folgt codiert:

1. ForAll(time, And(func1(time) >= 1, func1(time) <= 100))

   Bitte beachten Sie, dass ich die Zeitvariable explizit müssen universell quantifiziert werden, weil ich die Z3 gehen wollen, dass ich geben unsat wenn ich spritze Eigentum der folgenden Art:

2. Soweit mein Verständnis für Z3, alle Konstanten haben mathematische (theoretisch) und nicht Computer (praktisch) im geht plementation, d. h. ihre Werte sind nicht gebunden (leider kann ich nicht auf die Ressource zeigen, wo ich diese im Moment gelesen habe). Nehmen wir an, dass ich mit der Zeit die Zeit in meinen Systemen modelliere und gemäß den Systemeinschränkungen nicht mehr als x Stunden laufen kann, was ich verwenden kann und sage, dass der Wert der Zeit zwischen 0 und x * 60 '* 60 liegt, um das Maximum zu geben Ausführungszeit in Sekunden. Ich weiß, dass ich die erlaubten Werte für Zeit mit folgenden Behauptung geltend machen kann:

3. And(time >= 0, time <= x*60*60)

   aber wird es die universelle Quantifizierung in 1 gegeben beeinflussen?

Folglich sollte dies zu einer Situation führen, in der, wenn die Eigenschaft 2 injiziert wird und für Wert der Zeit ich angeben x*60*60 + 1, ist es nicht ungesetzt sein sollte, da die ForAll gilt nur für die Werte der Zeit.

Answer 1

aber wird es die universelle Quantifizierung in 1) beeinflussen?

Beachten Sie, dass

ForAll(time, And(func1(time) >= 1, func1(time) <= 100)) 

behandelt die Variable "Zeit" als gebundene. Die Formel hat die gleiche Bedeutung wie:

ForAll(xx, And(func1(xx) >= 1, func1(xx) <= 100)) 

Wenn Sie die oben behaupten, die Bedeutung ist, dass jede Instanziierung xx hält (geltend gemacht wird).Insbesondere können Sie die quantifizierte Variable mit der freien Variablen „Zeit“ und insbesondere instanziiert, können Sie mit x * 60 * 60 + 1 Herstellung der Behauptung instanziiert:

And(func1(x*60*60+1) >= 1, func1(x*60*60+1) <= 100) 

Sie Angenommen, wollte, dass

sagen

And(func1(xx) >= 1, func1(xx) <= 100)) 

für jeden Wert xx zwischen 0 und x * 60 * 60, dann können Sie schreiben, gilt:

poi

ForAll(xx, Implies(And(xx >= 0, xx <= x*60*60), And(func1(xx) >= 1, func1(xx) <= 100))) 

(leider kann ich nicht zu der Ressource, wo ich das gerade gelesen habe).

Vernünftige logische Lehrbücher oder Grundlagen von Informatikbüchern sollten dies genau erklären. Z3 unterstützt eine mehrfache sortierte Logik erster Ordnung (mit Hintergrundtheorien).