Neue Frage
0

Exists Algorithm

gefragt 2017-08-22 21:11:09 +0200

blackmamba Gravatar-Bild

aktualisiert 2017-08-22 21:11:25 +0200

So, I need to clear some basics for Exists Algorithm.

This is what I know so far.

∀x1 ∀x2. ϕ

e becomes x1 & x2. Then I will negate the ϕ (!(ϕ)) as the algorithm is for Exists.

Do we also have to change the Apply parameter from OR to AND?

bearbeiten retag Als beleidigend melden schließen löschen

1 Antwort

1

geantwortet 2017-08-22 21:24:57 +0200

PS Gravatar-Bild

By definition, we have

  • $\exists x. \varphi :\equiv [\varphi]_x^1 \vee [\varphi]_x^0$
  • $\forall x. \varphi :\equiv [\varphi]_x^1 \wedge [\varphi]_x^0$

By this, it is not difficult to see that

  • $\neg\exists x. \varphi \Leftrightarrow \neg([\varphi]_x^1 \vee [\varphi]_x^0) \Leftrightarrow \neg[\varphi]_x^1 \wedge \neg[\varphi]_x^0\Leftrightarrow[\neg\varphi]_x^1 \wedge[\neg\varphi]_x^0 \Leftrightarrow \forall x. \neg\varphi$

hence,

  • $\exists x. \varphi \Leftrightarrow \neg\forall x. \neg\varphi$
  • $\forall x. \varphi \Leftrightarrow \neg\exists x. \neg\varphi$

These equivalences remain all valid if quantification is done on more than one variable. The latter explains how you can reduce the universal quantification to the existential one, and for the existential one, you know how to do it, right?

And a direct answer to your question about replacing OR with AND in the call to APPLY in the algorithm: Yes, that is what will happen there, if you will directly implement Forall as a BDD algorithm.

bearbeiten Als beleidigend melden löschen publish Link mehr

Kommentare

So, first I negate the given phi. Then while solving the algorithm, I replace OR with AND. The confusion is do we have to do both the steps or only step will suffice?

blackmamba ( 2017-08-22 21:30:09 +0200 )bearbeiten

You only do one of the two, i.e., either use Exists with $\neg\varphi$ and negate its result, or use a direct implementation of the Forall algorithm that you obtain essentially by replacing the OR by AND. But I would have to check is further changes are done in Forall (e.g. in the base cases).

PS ( 2017-08-22 22:19:23 +0200 )bearbeiten

Ihre Antwort

Du kannst deinen Eintrag bereits als Gast verfassen. Deine Antwort wird zwischengespeichert, bis du dich eingeloggt oder registriert hast.
Bitte nur konstruktive Antworten auf diese konkrete Frage posten.
Falls du eine Frage stellen willst, dann stelle eine neue Frage.
Für kurze Diskussionen und Nachfragen benutze bitte die Kommentar-Funktion.
Deine Fragen und Antworten kannst du jederzeit nachbearbeiten und verbessern.
Gute Fragen und Antworten kannst du mit einem Upvote oder Downvote bewerten.

Schreibe deine Antwort auf diese Frage

[Vorschau ausblenden]

Fragen-Tools

Beobachten
1 Follower

Statistik

Gefragt: 2017-08-22 21:11:09 +0200

Gesehen: 201 mal

Letztes Update: Aug 22