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.
126 lines
5.0 KiB
126 lines
5.0 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(f(x)=x)$
|
|
\item $e_{1}\Leftrightarrow(f(x)=y)$
|
|
\item $e_{2}\Leftrightarrow(x=y)$
|
|
\item $e_{3}\Leftrightarrow(z=f(x))$
|
|
\end{itemize}
|
|
|
|
|
|
$\hat{\varphi} = (\clause{e_{0}; e_{1}; e_{2}}) \land (\clause{\lnot e_{0}; e_{1}}) \land (\clause{\lnot e_{1}; e_{2}}) \land (\clause{e_{2}; e_{3}}) \land (\clause{\lnot e_{2}; e_{1}}) \land (\clause{\lnot e_{3}; \lnot e_{1}}) $
|
|
|
|
|
|
\hspace{-0.09cm}\scalebox{0.85}{
|
|
\begin{dplltabular}{4}
|
|
\dpllStep{1|2|3|4}
|
|
\dpllDecL{0|1|2|2}
|
|
\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}, \lnot e_{2}$}
|
|
\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|$e_{2}$|\conflict}
|
|
\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done}
|
|
\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done|\done}
|
|
\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{3}$}
|
|
\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|$\lnot e_{2}$|\done}
|
|
\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|\done|\done}
|
|
\dpllBCP{ - | - |$\lnot e_{2}$| - }
|
|
\dpllPL{ - | - | - | - }
|
|
\dpllDeci{$\lnot e_{0}$|$\lnot e_{1}$| - | - }
|
|
\end{dplltabular}
|
|
}
|
|
|
|
Conflict in step 4\\
|
|
\scalebox{0.75}{
|
|
|
|
\begin{tikzpicture}[>=latex,line join=bevel,]
|
|
\pgfsetlinewidth{1bp}
|
|
%%
|
|
\pgfsetcolor{black}
|
|
% Edge: 1 -> 4
|
|
\draw [->] (21.08bp,83.506bp) .. controls (26.44bp,80.758bp) and (33.44bp,77.508bp) .. (40.0bp,75.5bp) .. controls (51.601bp,71.949bp) and (65.006bp,69.732bp) .. (85.898bp,67.281bp);
|
|
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
|
|
\pgfsetstrokecolor{strokecol}
|
|
\draw (54.0bp,83.0bp) node {$$1$$};
|
|
% Edge: 1 -> 5
|
|
\draw [->] (21.966bp,90.636bp) .. controls (35.227bp,93.477bp) and (58.98bp,98.567bp) .. (86.047bp,104.37bp);
|
|
\draw (54.0bp,107.0bp) node {$$5$$};
|
|
% Edge: 2 -> 4
|
|
\draw [->] (21.717bp,33.396bp) .. controls (33.05bp,36.904bp) and (52.243bp,43.253bp) .. (68.0bp,50.5bp) .. controls (71.462bp,52.092bp) and (75.062bp,53.969bp) .. (87.382bp,61.048bp);
|
|
\draw (54.0bp,58.0bp) node {$$1$$};
|
|
% Edge: 4 -> 3
|
|
\draw [->] (107.67bp,69.723bp) .. controls (115.24bp,72.246bp) and (126.02bp,75.839bp) .. (145.09bp,82.197bp);
|
|
% Edge: 5 -> 3
|
|
\draw [->] (107.67bp,102.94bp) .. controls (115.41bp,100.08bp) and (126.51bp,95.995bp) .. (145.47bp,89.01bp);
|
|
% Node: 1
|
|
\begin{scope}
|
|
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
|
|
\pgfsetstrokecolor{strokecol}
|
|
\draw (11.0bp,88.5bp) ellipse (11.0bp and 11.0bp);
|
|
\draw (11.0bp,88.5bp) node {$\lnot e_{1}$};
|
|
\end{scope}
|
|
% Node: 4
|
|
\begin{scope}
|
|
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
|
|
\pgfsetstrokecolor{strokecol}
|
|
\draw (97.0bp,66.5bp) ellipse (11.0bp and 11.0bp);
|
|
\draw (97.0bp,66.5bp) node {$e_{2}$};
|
|
\end{scope}
|
|
% Node: 5
|
|
\begin{scope}
|
|
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
|
|
\pgfsetstrokecolor{strokecol}
|
|
\draw (97.0bp,106.5bp) ellipse (11.0bp and 11.0bp);
|
|
\draw (97.0bp,106.5bp) node {$\lnot e_{2}$};
|
|
\end{scope}
|
|
% Node: 2
|
|
\begin{scope}
|
|
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
|
|
\pgfsetstrokecolor{strokecol}
|
|
\draw (11.0bp,30.5bp) ellipse (11.0bp and 11.0bp);
|
|
\draw (11.0bp,30.5bp) node {$\lnot e_{0}$};
|
|
\end{scope}
|
|
% Node: 3
|
|
\begin{scope}
|
|
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
|
|
\pgfsetstrokecolor{strokecol}
|
|
\draw (156.0bp,85.5bp) ellipse (11.0bp and 11.0bp);
|
|
\draw (156.0bp,85.5bp) node {$\bot$};
|
|
\end{scope}
|
|
%
|
|
\end{tikzpicture}
|
|
|
|
|
|
}
|
|
\begin{prooftree}
|
|
\AxiomC{$1. \; e_{0} \lor e_{1} \lor e_{2}$}
|
|
\AxiomC{$5. \; \lnot e_{2} \lor e_{1}$}
|
|
\BinaryInfC{$e_{0} \lor e_{1}$}
|
|
\end{prooftree}
|
|
|
|
\hspace{-0.09cm}\scalebox{0.85}{
|
|
\begin{dplltabular}{4}
|
|
\dpllStep{5|6|7|8}
|
|
\dpllDecL{1|1|1|1}
|
|
\dpllAssi{$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{2}$|\makecell{$\lnot e_{0}, e_{1}, e_{2}, $ \\ $\lnot e_{3}$}}
|
|
\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{1}, e_{2}$|\done|\done|\done}
|
|
\dpllClause{2}{$\lnot e_{0}, e_{1}$}{\done|\done|\done|\done}
|
|
\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$e_{2}$|\done|\done}
|
|
\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done}
|
|
\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|\done|\done|\done}
|
|
\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}$|$\lnot e_{3}$|\done}
|
|
\dpllClause{7}{$e_{0}, e_{1}$}{$e_{1}$|\done|\done|\done}
|
|
\dpllBCP{$e_{1}$|$e_{2}$|$\lnot e_{3}$| - }
|
|
\dpllPL{ - | - | - | - }
|
|
\dpllDeci{ - | - | - | - }
|
|
\end{dplltabular}
|
|
}
|
|
|
|
$\Model_{\EUF} := (f(x) \neq x) \land (f(x) = y) \land (x = y) \land (z \neq f(x)) $ \\
|
|
Check if the assignment is consistent with the theory:
|
|
|
|
\begin{align*}
|
|
&\{f(x), y\}, \{x, y\}, \{z\}\\
|
|
&\{z\}, \{f(x), x, y\}
|
|
\end{align*}
|
|
|
|
$\Model_{\EUF}$ is not consistent with the theory, because of: $(f(x) \neq x) $\\
|
|
$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $
|
|
$BC :=e_{0} \lor \neg e_{1} \lor \neg e_{2} \lor e_{3}$\\
|