\documentclass[12pt]{article}

\usepackage{a4wide}
\usepackage{amstext}
\usepackage{graphs}
\usepackage{color}
\usepackage{amsfonts}
\usepackage[swedish]{babel}
\usepackage[latin1]{inputenc}

\input{../defns}

\parindent 0pt
\parskip 5pt

\pagestyle{empty}

\begin{document}
F.\ Drewes, J.\ Högberg\hfill 2006-09-18

%\bigskip
\begin{center}
\bfseries%
{\large Logik för datavetare, HT05\\}
-- Latex-mall --
\end{center}

\bigskip
{\bf Blockvärldar}
\medskip
\graphfillcolour{1}
\begin{center}
\begin{picture}(2.5,3)
  \kub(0,0){$K_1$}
  \kub(0,1){$K_2$}
  \pyr(0,2){$P_2$}
  \pyr(1.5,0){$P_1$}
\end{picture}
\qquad är okej men inte\qquad
\begin{picture}(2.5,3)
  \kub(0,0){$K_1$}
  \kub(1.5,0){$K_2$}
  \pyr(.75,1){$P_2$}
  \pyr(.75,2){$P_1$}
\end{picture}
\end{center}

\bigskip
{\bf Ett bevis i Hilbertsystemet}
\medskip

Vi vill visa att $\{A, A\rightarrow B, B\rightarrow C\}\models \neg D\rightarrow C$.

\def\arraystretch{1}%
\begin{tabular}{@{}rll@{}}
1.&$A$&(hypotes)\\
2.&$A\rightarrow B$&(hypotes)\\
3.&$B$&(modus ponens på 1 och 2)\\
4.&$B\rightarrow C$&(hypotes)\\
5.&$C$&(modus ponens på 3 och 4)\\
6.&$C\rightarrow(\neg D\rightarrow C)$&($\ax_1=\alpha_1\rightarrow(\alpha_2\rightarrow\alpha_1)$ med\\&& $\alpha_1=C$ och $\alpha_2=\neg D$)\\
7.&$\neg D\rightarrow C$&(modus ponens på 5 och 6)
\end{tabular}

\bigskip
{\bf Resolution i satslogiken}
\medskip

Resolutionsregeln är bevisregeln
\[\fbox{\quad$\regel{\alpha\vee p,\ \alpha'\vee\neg p}{\alpha\vee\alpha'}$\quad}\]
där $\alpha,\alpha'$ står för godtyckliga klausuler och $p$ för en godtycklig atom.

\medskip
\begin{itemize}
\item[-] Resolutionsregeln appliceras alltså på klausuler $\varphi=l_1\vee\cdots\vee l_m\vee l$ och $\varphi'=l_1'\vee\cdots\vee l_n'\vee l'$ där $l$ och $l'$ är komplementära. Resultatet $l_1\vee\cdots\vee l_m\vee l_1'\vee\cdots\vee l_n'$ är igen en klausul, en resolvent av $\{\varphi,\varphi'\}$.
\item[-] Implicit stryks dubbla litteraler från resolventen, dvs vi tar alltid bort de $l_i'$ som redan förekommer bland $l_1,\dots,l_m$.
\item[-] Mängden av alla resolventer av $\{\varphi,\varphi'\}$ skrivs $\res(\varphi,\varphi')$.
\end{itemize}

\medskip
\begin{graph}(10.6,2.9)(-.2,1.3)
\roundnode x(7,1.8)[\graphnodesize 0]
\textnode 1(0,4){$A$}
\textnode 2(1.5,4){$\neg A\vee B$}
\textnode 3(4,4){$\neg B\vee C\vee D$}
\textnode 4(6.5,4){$\neg D\vee E$}
\textnode 5(8.5,4){$\neg E$}
\textnode 6(10,4){$\neg C$}
\textnode 7(2.5,3){$\neg A\vee C\vee D$}\diredge 37\diredge 27
\textnode 8(7.5,3){$\neg D$}\diredge 48\diredge 58
\textnode 9(5.5,2.5){$\neg A\vee C$}\diredge 79\diredge 89
\textnode A(7.5,1.8){$C$}\diredge 9A
\textnode B(9.5,1.5){$\bot$}\diredge AB\diredge 6B
\curve{.2}{(0,4,-90)(1,2.5,-45)(7,1.8,0)}[\filledareasfalse]
\diredge xA
\freetext(13.5,2.5){\protect\parbox{5.3\unitlength}{\raggedright\color{black}%
varken enhetsvederläggning eller inputvederläggning}}
\end{graph}


\bigskip
{\bf Hornklausuler och minsta modellen}
\medskip

För en formelmängd $\Phi$ låt
\[
\atcons(\Phi)=\{A\in\P\mid\Phi\models A\}=\{A\in\P\mid v(A)=1\text{\ för alla\ }v\in\M(\Phi)\}
\]
vara mängden av $\Phi$s \emph{atomära konsekvenser}. Tolkningen $v^{\Phi}_{\bot}$ definieras
\[
v^{\Phi}_{\bot}(A)=\left\{
\begin{array}{ll}
1&\text{om $A\in\atcons(\Phi)$}\\
0&\text{annars.}
\end{array}\right.
\]

\medskip
Observation: Om $v^{\Phi}_{\bot}$ är en modell av $\Phi$ så är den dess \emph{minsta modell} i den bemärkelsen att alla övriga modeller $v$ uppfyller $v(A)\ge v^{\Phi}_{\bot}(A)$ för alla $A\in\P$ (och om $v^{\Phi}_{\bot}$ inte är en modell av $\Phi$ så har $\Phi$ ingen minsta modell).

\bigskip
{\bf Första ordningens predikatlogik}
\medskip

En \emph{första ordningens predikatlogik} är en quadrupel $\L=(\R,\C,\A,\T)$ där
\begin{itemize}
\item[-] \R\ är en mängd av \emph{relationssymboler} där varje $R\in\R$ har en \emph{ställighet} $\arity(R)\ge 0$,
\item[-] $\C\subseteq\{\forall,\exists,\neg,\rightarrow,\wedge,\vee,\leftrightarrow,\bot,\top\}$ är mängden av \emph{konnektiv} (alltså som i satslogiken fast med ytterligare konnektiv $\forall,\exists$),
\item[-] mängden $\A$ som består av (, ) och , är mängden av \emph{hjälpsymboler} och
\item[-] \T\ är en signatur.
\end{itemize}
Det krävs att alla symbolmängder är disjunkta. Om inget annat sägs antas att $\C=\{\forall,\exists,\neg,\rightarrow,\wedge,\vee,\leftrightarrow,\bot,\top\}$.

\bigskip
{\bf Tolkningar}
\medskip

Låt $\L=(\R,\C,\A,\T)$ vara en predikatlogik där $\T=(\V,\K,\F)$. En tolkning $J$ av \L\ består av följande komponenter:
\begin{itemize}
\item[-] En icke tom men i övrigt godtycklig mängd $\dom(J)$, tolkningens \emph{domän}.
\item[-] En $n$-ställig \emph{relation} $R^J\subseteq\dom(J)^n$ för varje relationssymbol $R^{(n)}\in\R$.

Relationen $R^J$ betraktas som ett \emph{predikat} $R^J\colon\dom(J)^n\to\{0,1\}$ som tar objekt $d_1,\dots,d_n\in\dom(J)$ som argument och returnerar sanningsvärdet $1$ om $(d_1,\dots,d_n)\in R^J$ och $0$ annars.
\item[-] Ett objekt $K^J\in\dom(J)$ för varje konstant $K\in\K$.
\item[-] En $n$-ställig funktion $f^J\colon\dom(J)^n\to\dom(J)$ för varje funktionssymbol $f^{(n)}\in\F$.
\end{itemize}

\bigskip
{\bf Meningar}
\medskip

Variablerna inom räckvidden för en kvantifierare är alltså de som kvantifieraren syftar på. (Konceptet liknar räckvidden för en variabel i ett programspråk med lexikalisk räckvidd.)

\[
\begin{array}{c}
(\exists\red{\underline x})(\underbrace{(R(\red{\underline x})\wedge(\forall\green{\underline x})(\underbrace{Q(\green{\underline x},y)}))\vee(\forall{\color{black}\underline y})(\underbrace{Q(f(\red{\underline x}),{\color{black}\underline y})})})\rightarrow R(x)
\end{array}
\]

\bigskip
{\bf Skolemisering}
\medskip

Betrakta t\,ex  $\varphi=(\forall x)(\forall y)(\exists z)(\forall z')(\varphi')$ och en tolkning $J$ där $\varphi^J=1$.

\begin{itemize}
\item[-] Man ska alltså för alla $d_x,d_y\in\dom(J)$ kunna välja något $d_z\in\dom(J)$ som gör att $(\forall z')(\varphi')$:s värde blir $1$ under $J$-värderingarna som tilldelar $x,y,z$ värdena $d_x,d_y,d_z$.
\item[-] Värdet $d_z$ beror på $d_x$ och $d_y$ (men \emph{inte} på $d_{z'}$). Man kan alltså se det som en funktion $\textsf{choose}_z$ som väljer rätt värde beroende på $d_x,d_y$, dvs $d_z=\textsf{choose}_z(d_x,d_y)$.
\item[-] Vi kan därför utöka logiken med en ny (!) funktionssymbol $f_z^{(2)}$ och ersätta formeln med $\psi=(\forall x)(\forall y)(\forall z')(\varphi'')$ där $\varphi''$ fås genom att ersätta alla förekomster av $z$ i $\varphi'$ med $f_z(x,y)$.
\item[-] Om $J$ utökas på så sätt att $f_z$ tolkas som $\textsf{choose}_z$ så gäller $\psi^J=1$.
\end{itemize}

\newpage 

\bigskip
{\bf Resolution kräver substitution}
\medskip

\begin{center}

\fbox{
$\begin{array}{@{}r@{}}
\{(\forall x)(\forall y)(P(f(x),h(y))\vee Q(y)),\ (\forall x)(\neg Q(g(a)))\}\qquad\\
\models(\exists x)(\forall y)(P(f(y),h(g(x))))
\end{array}$
}
\end{center}

Normalisering ger klausulerna $\begin{array}[t]{l@{\ }l}
\black{1.}&P(f(x),h(y))\vee Q(y),\\
\black{2.}&\neg Q(g(a)),\\
\black{3.}&\neg P(f(f_y(z)),h(g(z)))\black.
\end{array}$

\begin{center}\unitlength=.9\unitlength\small\opaquetexttrue
\begin{graph}(12.4,4.5)(-.2,-.2)
\textnode 1(2,4){$P(f(x),h(y))\vee Q(y)$}
\textnode 2(6,4){$\neg Q(g(a))$}
\textnode 3(10,4){$\neg P(f(f_y(z)),h(g(z)))$}
\textnode 4(4,2){$P(f(x),h(g(a)))$}
  \edge 14
  \edge 24
  \nodetext 4(0,1){$\{g(a)/y\}$}
\textnode 5(6,0){$\bot$}
  \edge 45
  \edge 35
  \nodetext 5(0,1){$\{f_y(a)/x,\ a/z\}$}
\end{graph}
\end{center}


\bigskip
{\bf Resolutionsbevis 1}
\medskip

\vfill
\begin{center}\small\opaquetexttrue
\begin{graph}(13.4,8.5)(.3,-.2)
\textnode 1(1,8){$L(a,b)$}
\textnode 2(5.3,8){$L(f(x_1,x_2),g(x_3)) \vee \neg L(x_2,x_3)$}
\textnode 3(11.25,8){$\neg L(f(y_1,f(c,f(d,a))),y_2)$}
\textnode 4(3.15,6){$L(f(x_1,a),g(b))$}
  \edge 14
  \edge 24
  \nodetext 4(0,1){$\{a/x_2,\ b/x_3\}$}
\textnode 5(5.15,4){$L(f(x_1,f(x_1,a)),g(g(b)))$}
  \edge 45
  \bow 25{.2}
  \nodetext 5(0,1){$\{f(x_1,a)/x_2,\ g(b)/x_3\}$}
\textnode 6(7.15,2){$L(f(x_1,f(x_1,f(x_1,a))),g(g(g(b))))$}
  \edge 56
  \bow 26{.3}
  \nodetext 6(0,1){$\{f(x_1,f(x_1,a))/x_2,\ g(g(b))/x_3\}$}
\textnode 7(9.15,0){\red{ingen unifierare finns}}[\graphlinecolour 1]
%\textnode 7(9.15,0){$\bot$}
  \edge 67
  \bow 37{.15}
%  \nodetext 7(0,1){$\{y_1/z_4,\ c/z_5,\ d/z_6,\ g(g(g(b)))/y_2\}$}
\end{graph}
\end{center}


\bigskip
{\bf Resolutionsbevis 2}
\medskip

\vfill
\begin{center}\small\opaquetexttrue
\begin{graph}(13.4,8.5)(.3,-.2)
\textnode 1(1,8){$L(a,b)$}
\textnode 2(5.3,8){$L(f(x_1,x_2),g(x_3)) \vee \neg L(x_2,x_3)$}
\textnode 3(11.25,8){$\neg L(f(y_1,f(c,f(d,a))),y_2)$}
\textnode 4(3.15,6){$L(f(z_1,a),g(b))$}
  \edge 14
  \edge 24
  \nodetext 4(0,1){$\{a/x_2,\ b/x_3\}\,\sigma$}
\textnode 5(5.15,4){$L(f(z_2,f(z_3,a)),g(g(b)))$}
  \edge 45
  \bow 25{.2}
  \nodetext 5(0,1){$\{f(z_1,a)/x_2,\ g(b)/x_3\}\,\sigma'$}
\textnode 6(7.15,2){$L(f(z_4,f(z_5,f(z_6,a))),g(g(g(b))))$}
  \edge 56
  \bow 26{.3}
  \nodetext 6(0,1){$\{f(z_2,f(z_3,a))/x_2,\ g(g(b))/x_3\}\,\sigma''$}
\textnode 7(9.15,0){$\bot$}
  \edge 67
  \bow 37{.15}
  \nodetext 7(0,1){$\{y_1/z_4,\ c/z_5,\ d/z_6,\ g(g(g(b)))/y_2\}$}
\end{graph}
\end{center}

\bigskip
{\bf \ldots men varför kan $\Phi\vdash_{\Res}$ inte avgöras som i satslogiken?}
\medskip

\begin{center}\small\opaquetexttrue\unitlength=.8\unitlength
\begin{tabular}{@{}c@{}}\begin{graph}(10.3,10.3)(-1,-2)
\textnode 1(1,8){$P(x)\vee\neg Q(f(x))$}
\textnode 2(7,8){$\neg P(f(y))\vee Q(y)$}
\textnode 3(4,6){$\neg Q(f(f(y))\vee Q(f(y))$}
  \edge 13\edge 23
  \nodetext 3(0,.9){\scriptsize$\{f(y)/x\}$}
\textnode 4(2.5,4){$P(x)\vee\neg Q(f(f(x)))\}$}
  \bow 14{-.15}
  \edge 34
  \nodetext 4(-.1,.9){\scriptsize$\{x/y\}$}
\textnode 5(5.5,2){$\neg Q(f(f(f(y)))\vee Q(f(f(y)))$}
  \bow 25{.1}
  \edge 45
  \nodetext 5(-.4,.9){\scriptsize$\{f(y)/x\}$}
\textnode 6(2.5,0){$P(x)\vee\neg Q(f(f(f(x))))$}
  \bow 46{-.25}
  \edge 56
  \nodetext 6(0,.9){\scriptsize$\{x/y\}$}
\textnode x(5.5,-2){\phantom{$P(x)\vee\neg Q(f(f(f(x))))$}}[\graphlinecolour 1]
  \bow 2x{.3}[\graphlinedash{4 4}]
  \edge 6x[\graphlinedash{4 4}]
\end{graph}
\end{tabular}
\qquad
\parbox{12em}{\color{black}\raggedright Eftersom resolution innebär unifiering kan den generera \red{nya atomära formler}. Därför är sökrummet oändligt.}
\end{center}





\end{document}
