You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
|
\item \self Consider the following formula from $\mathcal{T}_{E}$. \begin{equation*} \phi_{EUF} := \big[ f_y = g_x \land f_y = y \big] \lor \big[ f_y = f_x \land y \neq f_{gy} \big] \lor \big[ f_x = f_y \land f_y = y \big] \lor \big[ f_x = f_{gy} \land f_y \neq y \big] \end{equation*} Use the graph-based algorithm to construct an equisatisfiable propositional formula $\phi_{prop}$.
What would you have to change if you would want to check $\phi_E$ for \textit{validity} instead of satisfiability?
|
