beseitigen forall mit unsat

Question

Wir wissen, dass wir Gültigkeit eines Satzes beweisen kann, mit den Worten:

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y) 
assert (forall (x,y) . Demorgan(x,y)) 

Alternativ können wir die forall quantifier beseitigen, indem er sagte, dass:

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y) 
(assert (not Demorgan(x,y))) 

Also, wenn es zurückgibt Ungesättigt, dann können wir sagen, dass die obige Formel gültig ist.

Jetzt möchte ich diese Idee verwenden, um den forall quantifier aus der folgenden Behauptung zu beseitigen:

assert (exists x1,x2,x3 st .(forall y . formula1(x1,y) iff 
              formula2(x2,y) iff 
              formula3(x3,y))) 

So ist es eine Möglichkeit, in Z3 (unter Verwendung von C++ API oder SMT-LIB2.0), dass ich behaupten kann etwa wie folgt:

assert (exists x1,x2,x3 st. (and ((not (formula1(x1,y) iff formula2(x2,y))) == unsat) 
            ((not (formula2(x2,y) iff formula3(x3,y))) == unsat))) 

Answer 1

Ja, wenn wir die Gültigkeit einer Formel, indem zeigt seine Negation unerfüllbar erweisen kann. Zum Beispiel, um zu zeigen, dass Forall X. F(X) gültig ist, müssen wir nur zeigen, dass not (Forall X. F(X)) unerfüllbar ist. Die Formel not (Forall X. F(X)) entspricht (Exists X. not F(X)). Die Formel (Exists X. not F(X)) ist equisatisfiable zu der Formel not F(X), wobei die gebundene Variable X durch eine frische Konstante X ersetzt wird. Mit equatisatisfiable, ich meine, dass der erste ist erfüllbar, wenn der zweite ist. Dieser Schritt, der existenzielle Quantoren entfernt, wird normalerweise skolemization genannt. Beachten Sie, dass diese letzten beiden Formeln nicht entsprechen. Betrachten Sie beispielsweise die Interpretation { X -> 2 }, die X zu 2 zuweist. Die Formel Exists X. not (X = 2) wird in dieser Interpretation immer noch als wahr ausgewertet, da wir X als 3 auswählen können. Auf der anderen Seite wird die Formel not (X = 2) in dieser Interpretation als falsch bewertet. Wir verwenden normalerweise den Begriff Quantifizierer Eliminierungsverfahren für ein Verfahren, das eine Formel F ergibt entspricht quantumfreie Formel F'. Daher wird die Skolemisierung nicht als Eliminierungsverfahren für Quantifizierer betrachtet, da das Ergebnis keine äquivalente Formel ist.

Das gesagt, wir müssen den Skolemisierungsschritt nicht von Hand anwenden. Z3 kann es für uns tun. Hier ist ein Beispiel (auch online verfügbar here).

(declare-sort S) 
(declare-fun F (S) Bool) 
(declare-fun G (S) Bool) 
(define-fun Conjecture() Bool 
    (forall ((x S)) (= (and (F x) (G x)) (not (or (not (F x)) (not (G x))))))) 
(assert (not Conjecture)) 
(check-sat) 

Nun, lassen Sie uns eine Formel der Exists X. Forall Y. F(X, Y) Form betrachten. Um die Gültigkeit dieser Formel zu beweisen, können wir die Negation not Exists X. Forall Y. F(X, Y) als unerfüllbar anzeigen. Die Negation entspricht Forall X. Exists Y. not F(X, Y). Wenn nun Skolemisierung auf diese Formel angewendet wird, erhalten wir Forall X. not F(X, Y(X)). In diesem Fall wurde die gebundene Variable Y durch Y(X) ersetzt, wobei Y ein neues Funktionssymbol in der resultierenden Formel ist. Die Intuition ist, dass die Funktion Y die "Wahlfunktion" ist. Für jede X können wir einen anderen Wert wählen, um die Formel F zu erfüllen. Z3 führt alle diese Schritte automatisch für uns aus. Wir müssen die Skolemisierung nicht von Hand anwenden. In diesem Fall ist die resultierende Formel jedoch normalerweise schwieriger zu lösen, da sie nach dem Skolemisierungsschritt einen universellen Quantifizierer enthält.