Z3: Modellierung mit Quantifizierern

Question

Ich möchte (∀i(0≤i<k→a[i]>0)∧a[k]>0)→∀i(0≤i≤k→a[i]>0) von z3 beweisen. Die Negation davon ist: ∀i(0≤i<k→a[i]>0)∧a[k]>0∧∃i(0≤i≤k∧¬(a[i]>0)). Zuerst habe ich den Wert von k bis 5 und ignorieren den Teil a[k]>0 und versuchen:

from z3 import * 
i = Int('i')` 
a = Array('a',IntSort(),IntSort()) 
solver = Solver() 
solver.add(ForAll(i, Implies(And(i >= 0,i < 5),a[i] > 0))) 
solver.add(Exists(i, And(i >= 0,i <= 5, Not(a[i] > 0)))) 
print solver.check() 
print solver.model() 

Die Ausgabe lautet:

sat 
[i!0 = 5, 
a = [else -> k!8!10(k!9(Var(0)))], 
k!8 = [else -> k!8!10(k!9(Var(0)))], 
k!9 = [else -> If(Var(0) >= 4, If(Var(0) >= 5, 5, 4), 0)], 
k!8!10 = [0 -> 7720, 4 -> 1, else -> -38]] 

Ich weiß nicht, die Bedeutung des Ausgangs und ich denke, Sein Modell sollte i = 5 sein. Dann füge ich in a[5] > 0 hinzu, und ich denke, dass es unzufrieden sein sollte. Der Code lautet wie folgt:

from z3 import * 
i = Int('i') 
a = Array('a',IntSort(),IntSort()) 
solver = Solver() 
solver.add(ForAll(i, Implies(And(i >= 0,i < 5),a[i] > 0))) 
solver.add(Exists(i, And(i >= 0,i <= 5, Not(a[i] > 0)))) 
solver.add(a[5] > 0) 
print solver.check() 
print solver.model() 

Und der Ausgang ist:

unsat 

Also, wie kann ich (∀i(0≤i<k→a[i]>0)∧a[k]>0)→∀i(0≤i≤k→a[i]>0) von z3py beweisen, und was ist der Sinn der Ausgabe?

Answer 1

Es ist mir ein wenig unklar, was Sie mit Ihren Anfragen zu tun versuchen. Warum setzt du den Wert von k? Dies scheint nicht mit dem allgemeinen Fall übereinzustimmen, was Sie zu Beginn der Frage zu beweisen versuchen, aber vielleicht ist der spezielle Fall alles, woran Sie gerade interessiert sind.

Sie haben Ihre Gültigkeitsfrage korrekt in eine Erfüllbarkeitsfrage umgewandelt: Die Negation der Formel ist erfüllbar, wenn die ursprüngliche Formel gültig ist.

In der ersten Antwort von Z3 erhalten Sie tatsächlich ein Modell; Dies deutet auf ein Gegenbeispiel zu der (schwächeren) ersten Implikation hin, die Sie zu beweisen versuchen. Wenn Sie darüber nachdenken, was die Demonstration dieses Gegenbeispiels erfordert, müssen Sie wählen, die (gebundene) Existenzvariable auf 5 zu instanziieren. Dies ist die Bedeutung von i! 0 im Modell; Es ist ein neuer (freier) Name, der das Element Ihres Modells darstellt, dem die existentiell gebundene Variable zugewiesen wird.

Betrachtet man diesen anderen Weg (genauer gesagt, in Bezug auf das, was das Werkzeug macht), wird der existenzielle Quantor "skolemisiert" (die existentiell gebundene Variable wird durch eine neue Konstante ersetzt), bevor Z3 die interessante Arbeit erledigt , so ist es tatsächlich eine Abfrage entspricht Abfrage satifiability der Formel Bekämpfung:

∀i(0≤i<k→a[i]>0)∧a[k]>0∧(0≤ i!0 ≤k∧¬(a[ i!0 ]>0)) 

Wenn Sie die Abfrage zurück auf die Negation des ursprünglichen Implikation stärken, erhalten Sie unsat von Z3. Dies bedeutet, dass diese negierte Formel unerfüllbar war, so dass die Implikation, an der Sie interessiert sind, gültig ist; Sie haben ∀i (0 ≤ i < 5 → a [i]> 0) ∧a [5]> 0) → ∀i (0≤i≤5 → a bewiesen [i]> 0)

Sie sollte das gleiche Ergebnis erhalten, wenn Sie k in Ihrem Problem auf 5 setzen.

In Bezug auf die anderen Informationen in der ersten Antwort von Z3 muss das Modell nicht nur einen Wert für (skolemised) i enthalten, sondern auch für das Array a in Ihrem Problem. Arrays werden als Funktionen dargestellt, die in einem solchen Modell durch Fälle definiert werden können; Der Fall "else" ist der Catch-All und der einzige Fall in jeder der hier verwendeten Funktionen. Var (0) ist die Syntax für den (ersten und einzigen) Parameter der Funktion. In diesem Modell wird das Array indirekt über die Zusammensetzung zweier anderer Funktionen definiert, k! 9 (was zur Identifizierung eines Teils der für das Modell relevanten Indizes zu verwenden scheint; in diesem Fall 0,4 und 5) und k! 8! 10 (definiert die Abbildung dieser Indizes auf Werte). Insbesondere speichert das Array in diesem Modell 7720 bei Index 0, 1 bei Index 4 und -38 bei Index 5 (keine anderen Indizes werden durch die Fälle von k!9. Definition; konzeptionell würde ich dies so verstehen, dass das Array in diesem Modell bei den anderen Indizes undefiniert ist).