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.
41 lines
2.2 KiB
41 lines
2.2 KiB
|
|
We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals:
|
|
\begin{itemize}
|
|
\item $e_{0}\Leftrightarrow(y=f(x))$
|
|
\item $e_{1}\Leftrightarrow(y=f(y))$
|
|
\item $e_{2}\Leftrightarrow(f(x)=z)$
|
|
\item $e_{3}\Leftrightarrow(f(y)=x)$
|
|
\item $e_{4}\Leftrightarrow(f(y)=z)$
|
|
\item $e_{5}\Leftrightarrow(z=x)$
|
|
\end{itemize}
|
|
|
|
$\hat{\varphi} = (\clause{\lnot e_{0}; \lnot e_{1}}) \land (\clause{e_{0}; e_{1}}) \land (\clause{e_{2}; e_{3}; \lnot e_{4}}) \land (\clause{e_{1}; \lnot e_{5}}) \land (\clause{e_{3}; e_{5}; e_{4}}) \land (\clause{e_{0}; e_{5}})$
|
|
|
|
\hspace{-0.09cm}\scalebox{0.85}{
|
|
\begin{dplltabular}{6}
|
|
\dpllStep{1|2|3|4|5|6}
|
|
\dpllDecL{0|0|0|1|1|1}
|
|
\dpllAssi{ - |$e_{2}$|$e_{2}, e_{3}$|$e_{2}, e_{3}, \lnot e_{0}$|\makecell{$e_{2}, e_{3}, \lnot e_{0}, $ \\ $e_{1}$}|\makecell{$e_{2}, e_{3}, \lnot e_{0}, $ \\ $e_{1}, e_{5}$}}
|
|
\dpllClause{1}{$\lnot e_{0}, \lnot e_{1}$}{$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|\done|\done|\done}
|
|
\dpllClause{2}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{1}$|\done|\done}
|
|
\dpllClause{3}{$e_{2}, e_{3}, \lnot e_{4}$}{$e_{2}, e_{3}, \lnot e_{4}$|\done|\done|\done|\done|\done}
|
|
\dpllClause{4}{$e_{1}, \lnot e_{5}$}{$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|\done|\done}
|
|
\dpllClause{5}{$e_{3}, e_{5}, e_{4}$}{$e_{3}, e_{5}, e_{4}$|$e_{3}, e_{5}, e_{4}$|\done|\done|\done|\done}
|
|
\dpllClause{6}{$e_{0}, e_{5}$}{$e_{0}, e_{5}$|$e_{0}, e_{5}$|$e_{0}, e_{5}$|$e_{5}$|$e_{5}$|\done}
|
|
\dpllBCP{ - | - | - |$e_{1}$|$e_{5}$| - }
|
|
\dpllPL{$e_{2}$|$e_{3}$| - | - | - | - }
|
|
\dpllDeci{ - | - |$\lnot e_{0}$| - | - | - }
|
|
\end{dplltabular}
|
|
}
|
|
|
|
$\Model_{\EUF} := (y \neq f(x)) \land (y = f(y)) \land (f(x) = z) \land (f(y) = x) \land (z = x) $ \\
|
|
Check if the assignment is consistent with the theory:
|
|
|
|
\begin{align*}
|
|
&\{y, f(y)\}, \{f(x), z\}, \{f(y), x\}, \{z, x\}\\
|
|
&\{f(x), f(y), x, y, z\}
|
|
\end{align*}
|
|
|
|
$\Model_{\EUF}$ is not consistent with the theory, because of: $(y \neq f(x)) $\\
|
|
$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $
|
|
$BC :=\neg e_{2} \lor \neg e_{3} \lor e_{0} \lor \neg e_{1} \lor \neg e_{5}$\\
|