\documentclass[12pt,a4paper]{scrartcl} % KOMA article \usepackage[T1]{fontenc} \usepackage[latin1]{inputenc} \usepackage[danish]{babel} \usepackage{xspace} \usepackage{times} \setlength{\parindent}{0em} \setlength{\parskip}{1ex plus .1ex minus .1ex} \setlength{\itemsep}{0ex} \begin{document} \section*{DM22 -- Eksamensopgave 2000 Januar 5} \subsection*{a)} Vi skal omskrive følgende logiske udtryk til konjunktiv normalform: \[ \neg (\forall X : p(X) \Rightarrow [ (\forall Y : p(Y) \Rightarrow p(f(X,Y))) \wedge \neg (\forall Z : q(X,Z) \Rightarrow p(Z)) ]) \] Dette foregår i 6 ½ trin som angivet på side 225 ff. i Cloksin og Mellish \textit{Programming in Prolog}. \subsubsection*{½. Omdøbning af variable} Dette trin er ikke nævnt i bogen, men kan nogle gange være nødvendigt. Hvis det samme variabelnavn er nævnt i forbindelse med flere $\exists$ og $\forall$, skal dette omdøbes, så navnet ikke går igen: \begin{itemize} \item $\exists X : p(X)$ \ldots $\exists X : q(X)$ er ækvivalent med $\exists A : p(A)$ \ldots $\exists B : q(B)$. \item $\forall X : p(X)$ \ldots $\exists X : q(X)$ er ækvivalent med $\forall A : p(A)$ \ldots $\exists B : q(B)$. \end{itemize} Tilsvarende for de andre kombinationer af $\exists$ og $\forall$. I vores udtryk er der ikke nogen variabel-navne, der går igen, og vi har derfor stadigvæk: \[ \neg (\forall X : p(X) \Rightarrow [ (\forall Y : p(Y) \Rightarrow p(f(X,Y))) \wedge \neg (\forall Z : q(X,Z) \Rightarrow p(Z)) ]) \] \subsubsection*{1. Fjernelse af implikationer} Vi kan bruge reglerne fra p. 223 for følgende: \begin{itemize} \item $ p \Rightarrow q $ er ækvivalent med $ \neg p \vee q$. \item $ p \Leftarrow q $ er ækvivalent med $ p \vee \neg q$. \item $ p \Leftrightarrow q$ er ækvivalent med $ (p \wedge q) \vee (\neg p \wedge \neg q)$. \end{itemize} Vi kan dernæst gå i krig med udtrykket, hvorved vi får: \[ \neg (\forall X : \neg p(X) \vee [ (\forall Y : \neg p(Y) \vee p(f(X,Y))) \wedge \neg (\forall Z : \neg q(X,Z) \vee p(Z)) ]) \] \subsubsection*{2. Flytning af negationer indad i udtrykkene} Denne gang skal vi benytte følgende regler, således at alle negationer kommer til at stå umiddelbart sammen med de enkelte prædikater. \begin{itemize} \item $\neg ( p \wedge q) $ er ækvivalent med $ \neg p \vee \neg q$. \item $\neg ( p \vee q) $ er ækvivalent med $ \neg p \wedge \neg q$. \item $\neg (\exists X : p(X)) $ er ækvivalent med $ \forall X : \neg p(X)$. \item $\neg (\forall X : p(X)) $ er ækvivalent med $ \exists X : \neg p(X)$. \end{itemize} Denne gang sker omformningen ad flere omgange: \[ \exists X : \neg (\neg p(X) \vee [ (\forall Y : \neg p(Y) \vee p(f(X,Y))) \wedge \neg (\forall Z : \neg q(X,Z) \vee p(Z)) ]) \]\[ \exists X : p(X) \wedge \neg [ (\forall Y : \neg p(Y) \vee p(f(X,Y))) \wedge \neg (\forall Z : \neg q(X,Z) \vee p(Z)) ] \]\[ \exists X : p(X) \wedge [ \neg (\forall Y : \neg p(Y) \vee p(f(X,Y))) \vee (\forall Z : \neg q(X,Z) \vee p(Z)) ] \]\[ \exists X : p(X) \wedge [ (\exists Y : \neg (\neg p(Y) \vee p(f(X,Y)))) \vee (\forall Z : \neg q(X,Z) \vee p(Z)) ] \]\[ \exists X : p(X) \wedge [ (\exists Y : p(Y) \wedge \neg p(f(X,Y))) \vee (\forall Z : \neg q(X,Z) \vee p(Z)) ] \] \subsubsection*{3. Skolemisering} I dette trin skal vi fjerne alle $\exists$-udtryk ved at bruge skolemisering. Dette svarer til at bruge følgende regel: \begin{itemize} \item $\exists X : p(X)$ laves om til $p(x)$ -- hvor $x$ er en hidtil uanvendt konstant. \end{itemize} I tilfælde hvor vi har et udtryk af typen $ \forall Y : \exists X : p(X)$ kan $X$ afhænge af $Y$. Denne sammenhæng udtrykkes ved at lave $X$ om til $x(Y)$ -- i dette filfælde får vi derfor udtrykket $ \forall Y : p(x(Y))$. Dette giver følgende resultat: \[ p(x) \wedge [ (p(y) \wedge \neg p(f(x,y))) \vee (\forall Z : \neg q(x,Z) \vee p(Z)) ] \] \subsubsection*{4. Flytning af universelle kvantorer udad} Kort fortalt fjerner vi blot alle $\forall$ operatorer -- dette giver følgende resultat: \[ p(x) \wedge [ (p(y) \wedge \neg p(f(x,y))) \vee (\neg q(x,Z) \vee p(Z)) ] \] \subsubsection*{5. Distribution af $\wedge$ over $\vee$} I dette trin søger vi at få alle og-operatorerne yderst i udtrykket. Dette gøres vha. følgende regel: \begin{itemize} \item $p \vee (q \wedge r)$ er ækvivalent med $ (p \vee q) \wedge (p \vee r)$. \item $(p \wedge q) \vee r$ er ækvivalent med $ (p \vee r) \wedge (q \vee r)$. \end{itemize} I vores tilfælde får vi: \[ p(x) \wedge [ ( p(y) \vee ( \neg q(x,Z) \vee p(Z)) ) \wedge ( \neg p(f(x,y)) \vee ( \neg q(x,Z) \vee p(Z)) ) ] \] \subsubsection*{6. Sammensætning af det hele} I dette sidste trin sætter vi de enkelte udtryk sammen, således at det hele ser ``pænt ud''. Hele udtrykket bliver dernæst (næsten uden forstyrrende parenteser) og nu i ``konjunktiv normalform'': \begin{itemize} \item[] $\left( p(x) \right)$ \item[$\wedge$] $\left( p(y) \vee \neg q(x,Z) \vee p(Z) \right)$ \item[$\wedge$] $\left( \neg p(f(x,y)) \vee \neg q(x,Z) \vee p(Z) \right)$ \end{itemize} \subsection*{a½)} Nogle gange bliver vi yderligere bedt om at skrive udtrykket i clausal normalform. Dette betyder kort fortalt, at vi for hver linie i konjunktiv normalform skal gøre følgende: \begin{itemize} \item $A_1 \vee A_2 \vee \cdots \vee A_i \vee \neg A_{i+1} \vee \neg A_{i+2} \vee \cdots \vee \neg A_{n}$ skrives som \\ $A_1 ; A_2 ; \cdots ; A_i$ :- $ A_{i+1} , A_{i+2} , \cdots, A_{n}$. Dvs. ikke-negerede udtryk på venstre side af ``:-'' adskilt af ``;'', mens negerede udtryk kommer på højre side af ``:-'' adskilt af ``,''. \end{itemize} Vi får derfor: (clausal normalform) \begin{itemize} \item[] $p(x) $ :- $.$ \item[] $p(y) ; p(Z) $ :- $ q(x,Z).$ \item[] $p(Z) $ :- $ p(f(x,y)), q(x,Z).$ \end{itemize} \newpage \subsection*{b) Lineær Inputresolution} Som udgangspunkt har vi følgende udtryk: \begin{itemize} \item $ \neg p \vee \neg q \vee r $ \item $ \neg s \vee t $ \item $ \neg t \vee p $ \item $ s $ \item $ \neg r $ \item $ \neg s \vee u $ \item $ \neg u \vee q $ \end{itemize} Vi skal vise, at udtrykkene er inkonsistente vha. lineær inputresolution som beskrevet p. 237. Som angivet p. 234 svarer dette til at kunne udlede et ``tomt'' udtryk ud fra de andre. Kort fortalt er det følgende regel vi skal benytte: \begin{itemize} \item $( X \vee A_1 \vee A_2 \vee \dots A_k)$ og $(\neg X \vee B_1 \vee B_2 \vee \dots B_l)$ giver følgende nye udtryk: $ A_1 \vee A_2 \vee \dots A_k \vee B_1 \vee B_2 \vee \dots B_l $ \end{itemize} Efter få overvejelser får vi følgende resultat: \begin{center} \begin{tabular}[hH]{c|c} Ved resolution med & fås:\\ \hline - & $ \neg r $ \\ $ \neg p \vee \neg q \vee r $ & $ \neg p \vee \neg q $ \\ $ \neg t \vee p $ & $ \neg q \vee \neg t $ \\ $ \neg u \vee q $ & $ \neg t \vee \neg u $ \\ $ \neg s \vee u $ & $ \neg s \vee \neg t $ \\ $ \neg s \vee t $ & $ \neg s $ \\ $ s $ & - \end{tabular} \end{center} Hvorved vi har vist det ønskede. \end{document}