Auswertungsspiel (Prädikatenlogik)

Das Auswertungsspiel $\mathfrak{G}(\mathcal{A},\phi )$ für eine Struktur $\mathcal{A}$ und eine Formel $\phi$ (in Negationsnormalform) wird wie folgt gespielt:
Die Positionen sind Paare $(\psi ,\beta )$, wobei $\psi$ eine Unterformel und $\beta$ die aktuelle Belegung ist.

Die Spielregeln:

• $\psi ={\psi }_1\vee {\psi }_2$: Verifiziererin wählt ${\psi }_1$ oder ${\psi }_2$. Das Spiel geht weiter mit der gewählten Teilformel.
• $\psi ={\psi }_1\wedge {\psi }_2$: Falsifizierer wählt ${\psi }_1$ oder ${\psi }_2$.
• $\psi =\mathrm{\exists }x\vartheta (x)$: Verifiziererin wählt ein Element $a\in \mathcal{A}$. Das Spiel geht weiter mit $(\vartheta ,\beta [x/a])$.
• $\psi =\mathrm{\forall }x\vartheta (x)$: Falsifizierer wählt ein Element $a\in \mathcal{A}$. Das Spiel geht weiter mit $(\vartheta ,\beta [x/a])$.
• $\psi$ ist Literal (Atom oder negiertes Atom): Das Spiel endet.
  • Ist $(\mathcal{A},\beta )\models \psi$, gewinnt die Verifiziererin.
  • Sonst gewinnt der Falsifizierer.