From a7731b88d4123d835cf6e0f1e5d44b98623c104a Mon Sep 17 00:00:00 2001
From: NotXia <35894453+NotXia@users.noreply.github.com>
Date: Mon, 4 Dec 2023 21:31:43 +0100
Subject: [PATCH] Add FAIKR2 Prolog basics
---
.../module2/img/_sldnf_correct_example.drawio | 119 ++++++++
.../module2/img/_sldnf_correct_example.pdf | Bin 0 -> 19742 bytes
.../img/_sldnf_incorrect_example.drawio | 48 +++
.../module2/img/_sldnf_incorrect_example.pdf | Bin 0 -> 18211 bytes
.../module2/main.tex | 1 +
.../module2/sections/_prolog.tex | 287 ++++++++++++++++++
6 files changed, 455 insertions(+)
create mode 100644 src/fundamentals-of-ai-and-kr/module2/img/_sldnf_correct_example.drawio
create mode 100644 src/fundamentals-of-ai-and-kr/module2/img/_sldnf_correct_example.pdf
create mode 100644 src/fundamentals-of-ai-and-kr/module2/img/_sldnf_incorrect_example.drawio
create mode 100644 src/fundamentals-of-ai-and-kr/module2/img/_sldnf_incorrect_example.pdf
create mode 100644 src/fundamentals-of-ai-and-kr/module2/sections/_prolog.tex
diff --git a/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_correct_example.drawio b/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_correct_example.drawio
new file mode 100644
index 0000000..a17f79b
--- /dev/null
+++ b/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_correct_example.drawio
@@ -0,0 +1,119 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_correct_example.pdf b/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_correct_example.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..cbac2256557142c466c782487494ab9d8e06c302
GIT binary patch
literal 19742
zcma&NV{m3&`|aCFI#wqg+qRuf(y?vZwr$(a9ox2T+s++(KhL}0bIyNPojP?^&HB|E
zV~(m-YtH#;t?MF{`zu1rNXHIC>i^FL1H;Hjz(8PYU;)F!14A!mY-8$V#z?@#&dkOF
zLoZ@(f0cLf(rJNL1RI4Q)KvsX$GsgE=Fjq(B(N-RY?U%
z{z0kys+25KsS2=$|4c4eRwxCp5;WPq;bhjgclZ7L@VR;ax_7b3xmlZWY(C+f;dCS)
z3>%g3CQ-EAs1#cQhs~`aGl(T>ey@aH;IiOerz0M}BCGfIodbvUU{$p|`6Uif#NTRm
zg|!oSvNJ1aWcEWn<%zB%Z||9(;Wwozk(F-qZh?+N0+M@dV3IL4y=I0N0dXQl2r&OS
zm0rEp?K=h-+gF2rR+viM-x%rb&oHjI2ZUYL@=z>9?L1-)>(DozDFA!59e{yr$#jVyOR?QO#?RD{6?uG
zTp6N+sSI2%BMNMaVo9!f;=Mn)>=8=%=0TbfcclP?4B1FC%&I({_B6Ue=f-rOX-lCP
zWGdMcwLg+^hNM+|>BO%9TW>T{bngK-pHIcd=$WR66gT9_Atjf0c0SwhXZ+}cM$x6x
z_1bC`S21RI;=f%)sqW4Dl34tyyM%ROA
z!@KW}{$xA0J0CBm$un^$*fq8t{yX}xRnewz-`V#xq_vZer-p+hmn`{5Zm)JW0(;=~
zp$*rjtAw{I;SHo+g@9?FF9mK7vJ?C1JHd?V`meVT7j0-!+4~oZl|Q25cpjWrre=;j
zSE+e~c+&628G#nhX4xg{sJ8AuKSN5euPz>Ev6U6=7enQR%-tB%C
zxixD+W7i;_IZ-NL`p=|bQPKJi8HX0sHgV_l&(Mj#mMa8}$lb;Tx_okoKrJ$l`28d9
zxj+i#0dyWDEHK`ojk+JK4@5PHUg&;^HHJvpxzpU>`9}sO(?5EK3^o-$_YLa=AB>M$
znoY|v5cwdfXA6^wT>LSj7v9s#0pweXxx4)*2JxpiqgvVl^%cUCL!(U`yt0-ulVe7W
z;jz;&^4Efl-3NbPNr^^~+kf!9n$e@3O17Ah)W{C%lBhtfTw2Ohj>r4lKCqgBubiXn
zqln!Tp1O>OUc{q2q)Q?cpYi{``0L?ffRXTsM`GZbp^#hLn2Aa}ncHy+=#`m$bmHxZ
zY5RMLo7S=A#HlT`6Uw7u&U;AR&vk05*3@B6Px407jy;18wMN)>VeSgN!MJE)MBwp-
z-oF-kA$2J}OzDg}*vcUC$RuUWW$5_$Rb_m!#((%)`falq7w1AoZpf=8$Wa1+WO5C)mVYC+Q^J%xaaXho-B`&M;BXs)T4eQe_U|ncCL1FleNXsgmhY
zgyHrCYt)su&+ce4D%OOl+!X5%&ju7%hH8)b^s+TArie(hrLF8Dg2}=PMl55OA2|U3_Jp&0<(eg((%U*Q?^Z(zqP};kv9_N
z4u#F`;KzEPBIm(znZap!(SZ(xhvu}}5p2GYhF{u^9~yU?0eBxcJh}O%jCAj(HBL#G
z>SPTJ?2-GJ6T^k7xK{8T>01+cM&Dz6M!Ax3w9w*(#b@(OlP90^lJgt$_(yBNnL}LQ
z25ay>`e5fqen37Lhc%a%4@V+bwMnFsADmj%Ma=^5H<+5
zlg|ViT7hltTHl*g-{I}#>XJ;tPt*tKIPnQ}@D2eiaBH{B#^kS{4ve^v&D7N
z7tz)j!W@ZtqS^hF6^OM-v6^ki+FGM9)_l}5PpC2%l0ru4CNn8+2b|@7XhH~Hyw33Y
zRcMxUsM03<*%ln9xnPB4Eo5UY=HTkdq!^nEvC4Z}+$8o~&d8ZP8x47{rGZ07UThJ?
z@@uveVn$0e%o$+pX71jK@bE?4qyT>&|4iyN3<3~)s2{Dlk&%Q9YcA^m(FGA*Jc_Re
z_`vOe_Bep^$mKkP97`UW0il2>{;#%_QMAekzL8U
zQ%@xy$l617xxPXVZ1HdSzka=2xgkERz+N^DGG2n9lb?{zNcljxJCfXpv5{>XwiLt)
zv%tN+p+21BrlmqMHsj9Pl{-NwQV58i5r~{>7ug2Fdk|as*>Fj+W2?*sujW4)h$vLp
zLpxm&Lye_TbG!IqhseY#rQ(7TIQq`Dwa#a^`;Odc`s8A*TNg}7pn8D
zGx!&9h#n_n+Dxa?c`c8lo|?}T$wr3R*`g|Hu(?Z`OWMnsu*#rPL&qf~BLank{Xu(X
zF6?8+XB>}?IT~=)T`~=tj53&|L;`gHOQXnzz~$aS8(p4N+?AhTrddeGd%d84X*fs=
zxUYp42N&)Ky|;)mZyvI!9OynJWLT3GdE*l)yCE!~Qr|Vex?irLL3Ri-*$ctGG|7H)
zdEW*0^Gm<53LuUC?Y$9&*0sC_LU(gqJT(oIS8I3YH+h1dU(7Hx{nSWF>pxnw9rt4g
z>vogLYso!|GVLcmYFvIk$chhF8M+7kt#MG@`*S;}Rco(VexeWS
ze-q?3ee~`q3nAauRebQKsCa(_U)4tK#nY-k@YwxwjEM^7a`!rN!Kr~4An%WkD?in>>I!#8k)
ze!0=`&$j9Hm-;|jr@61Gq@Fuw=OEMFs9KfHUACw#;5ig}tM_&L+hC;9^P{NT_SnpHnj$03_xsc`=sg3vaH@cL|i8+;w_sX%_wT!j3^M
z;kCQ10gTXyjhsfHhyit9!+MJ_)b+&h??#03-PAF4(cjRdNY*)Yf-DD)EFp`x{B?#P
zAqPaSa4DA6@%z%=KfP3Jv6RdSLGQXTam#9B(T)-0u%MlXi*0i1ElEf{5oFJ>#X03W
zx&4mbi&}lhVz2|qzbYe`E1ccEvpB!m$0QZb6ivZPrqfpTEVpK}@ixjDWMPZvM{>j@
z-}lvNaUHsop2T14#fBt!PX3zUoidED3coCbCwIEZ+4d@+Fix^FRy*a!_sb;ieAA<0
zN#PwA2RYWOwWr^`&7SSq1A=8ObKC=?AS?ss7uW9DtQfMlAI|by+bC>k`pd&i(S~UI
zbCp?k8z-S(_fxKkD1Kc)AND43;@%v-b9>`Z1pd2w3@3{$S8mm!#+R2}-uoiWxh
z@i!rBxL^#Yn(dj~@38U9byK0Hu1y&-#Aar;p
zWc!eK4v|QRVx_DE0~C}fB@CNL2-Y$bXOb2O`w%59T`E^`t`-nV7}+(13Q!R;St;+A
z%jU^z4&}k2OQ(?FD#FCc7g6d7DT647Cf})5;cpfa`C>v&DG?@6X(Lb*Ifz*)ldLHw
zaE+fD{v%@fQhCvpf4C`oX?9Z&39uP7^Aaz|=qW;RdbRxN#$~<|fuqoq0GwS4f17b>
zpO}VN*i+Qg!p=j}+K_vHa8R&A8NA@Fa}YFWxCBHsDey7k+F;Ip2*?z9eIPzZpCb)`
zNG~m5OjiHGF-ne+L4vebVt1!3Lc)JZ38FGz4#=>iz-iam%ZMU_*B@R9szzR$L)2@p
z6n?J}*eg;F8UwJ%iZN7zRWfI(4Id`?mY4$7G^4QtT>{bc&+T2Wfs`q*?`19p0W6Iz
zLS+da_$&J354c2u0ODb?=xU=g67c1@S;0)9vcze}5be=UI5IW-9nBPgKV;%?PUbQH
ztk(C+?B<%|Wkd61mVnHFTm$Gb5O`A8{qDK
zBpefbi;SJn?Am%!7eOZWc+P+3(A$wtf$97)B@fl3biB-W^y^wo{_slz;+oGjjcqhhNvfU02;%e}1!PFl;
zkRP;L5~-l<^Txd!r@%vQCvI(!PNCiBGwxpQv+=_Xr_|mKbKF}zja;wDYg9Mjc7&H7xA1S!TTotcY(MY|G81}+*PcvviJf3?
z<^5ylo)bFG08Z4m_Wt~Z(PO%EGiPkOzd>7OamQ9DWp*H+U~%%e{Wbk-_9pGoZzOu2L)J1oz$^qyOb6lE9=*iQC
z^$PUKIb?T`{oxDd<-c7(+uH)(Ep&HC_eN_C-c5bW>p|6)_%yrF+XcD^r=F
z@bvf1v+hMS^8|8YA-BfnfPcm3NM7fCqr8xN;I-zufP72QljIhIJ;3gUJ`mj!@4CFD
z>41I(e}TO~cV%sg_!jGeBF5zJg?tg-Ldh)7>^8oN
z0L|Z|c26G2ZgU^7chP$Rr;;A9Zc*DHc#wSIi5Is1&>rY%Mb8PE-pdYH9-J(
zu#D>$qEq|#ceqT=FD_mpCy&3U52rnq3nMVud@838T=@$Z!7?@IT;5r;XYe}(3xbXq
z4B8L0Mg+QCH&uDkXDGDpM50H?x3Yik$47T`wO27jJ%x`taEaD*csVXy`nk{ugz
z#DT!<`-=3pcU89jogMD8v`hZH;0EF7oG}cRf{^MTQEkS%~M
za6eBwk6l1yy>#xEot33Ed#Qu@vi)G-4MV^YDX;2d--SCu!!^x=co~4!`$5$SO+A
z3Yqfa%nmGt6H`UW8RI!
zNAp!xl~~@M$#f`hc0$qEtu_sK{)3Es4@p(=x9-C~JaHcHG?pwgi?|A$^i9@x5$oj7X!R3&m~U8L$+P^&|S$R
z6+*!CPyIu+6W`AX>Q9%v;d5)O6d&qr(*B|nu4nu1>_)J
z_`9tKrIvhga~@~hPHl^b
zG8e^?0;&FVklG+18uV2l+He}M?SBU!0#y7}0_l($sRhve=zczir5)v==H34}AufUB
zNrA%S-JJvb7sPH4exiu~BKE(|KX$up7L~{c{?uSrW0sVt
z1icZa5z8q)OdY!YhZA9`=pYSb)sJk*{l}Haw+ne+-t!vK&&PrlqFNPPsL5J(JRegc30#ZNdQyNALNnOwk}IX{)rTj{39v+<|W5&24a>U#)<8OPzvi*9hMGz{=+%oI6O@~Z!M2A
zuVHYJzVN=+G<;%!Q
z!7TEuLOdV-BD}^A4GM#4h-|QP&}?dh;{dKd*?I0nCTM0Zzu}baGUz#){1ve|q>-}L
zd&}Veg|wXo7=Z0R==J(8moU)Jrp+anWvlsHy>w)wy^~&1S)c-L-n6(?EFh?8AEU&5>r
zh!56n+)I7n!QiPeBErjz@TDxo2lE~c_U%f)I@fMZ&;rk{t^dM95&!w;Jb$Tv`O>@S
zx5bU-7v*+q&$K6hEcUGpvN-1U(pQ{oc+X@92P!Z7QKQ|7xozRMy)6f-VopSQqVXh?
z4UW;qqQ&R1?m4^51-r;2w$NL&@msXO=dj?XNR3aS<_*Itd_A@
zPT-ig1?P8gt`NXZ6tGu{dQB>6R8IgULyDGQifzAXxPI-mP0C=TrzE8qIl4O
zHn$ku{bJex8aT;fsH25#W@7)Yl)=@(=_G%>*lM}F_)>{^&jnFD?6wnB#^<$Polewh
zDQL<=(HR)ETO;wV{Bp7I#rHy9{5iUViT^u;t5kM6Di&Tk8hc~r`qcE&GaG8C7+Y@Q
zGDaZfP=4k3UiG^f$#C1!cI?CkxUR{?J=VsSg540?vLu~#3qPAZJUb?PElz*3<&$pl
z#FziveBQO>Vf$z105C0hI86S4t@((}h*UPJ<@!-w*1)wd&d!zcBsEky1*?cvn4jdKm8YYZ?P6z-D;nr8IaiKc@;r6+3Y6Hn=VVqK0{a
z1CB0o4{ft&Z=Pch(@B6*T)Z>K3-?xN?rebj(K4PdMW9hMY0v1v4Ay%S5BRrW&c5yB
z@3-cegkxK2uE&AqIVrY9ej8d}$p-G(_MeNmJ?2-yO}8DvTwCmDL!mQtj=(KgblQ{a
z0MbA!idrKc1MrU7mWt(2RCi3Be^WBs~)(&R_g
z*e5eP(|FS4lwr-_8PG(xO|ln3-}f_EcWtM-FCWyL<|N+IHWv}lfG_BLgeqw5pq|+w
zawwLQ4)U?B9Gf1eIpJ&`AZJ$jOIc`c4aWW|R{y>vB0Nk9
ze<|q^p$_gH#^RI$f-O<`x(rE;5NY;h0V_K3$WW3)&mMC^oC9Zo++Em-!PkXc_&1qq
zgVe;1>cRrYQsDxA3Whmrs4>%7W2mwEIP*DcC}ta+V$CSLv}z2C6t+!TwbwF(G^S0S
z+JGGxVBD-}%9a|q@iD>Tv`K!$Rc&#G@ygOs%PV$0NcU=J?Z>lNWTI8A@1Ys9b;x0Z
zD|NkoUO!wJIDb$c{T;_8LFKGSe>QrQ-4*TqC%|x}ac>ssHbPlM9lZjR*<nOdCIAg@sRTJFdfFt{}M${z$k`BI5*dxK_5ss_WRFwF%z%
zI^k>3GLwy5=YswziS-bI?xu%gn!Qf;cSq5QFtz24sldL^Ic9;8a
z>@D4WkqMaUQ{AoDl)CrdGoz*qkeHN3RI9$vzdUn_Hq0T<(tSD_fmaz
zl8(z>OW;DslJo_GhHZYuEEhDL7-MhS!PTd}&uJX>I&H6q@d9GjeynJgC(WT`3)?-W|r(&OWUh^^@zr
zmnj3s2F@3*3$P+VYel1w6iJ8;VvOFb_&Vq(PHv6gv$Rvz#~bd
zQ-p=)fNCr%m=zJqBNhft$7zfv5ypd)b(5vE7O^J6xO11K4O6Qo787R7Eym?T7U3G@
zDP{S`4uGyj4YfJ_Y)yNiAzoB2ins$=6*ClRBkpfHK6kChAXXF;i9%)b2Mr#bNNxor
zlj|@GW!iFiR)M|JW1^~UJr?6MW?HlhmovUI$a%yisTm`OQJO8@=Fc`cV@ZjXC9OgcALiN(9EpjV!baEz;JuGA3l^gei+Ee+Ltj`7)cU>DwlKMgazjjc;xSz^Ld1-KZ#emYbganINKa&GfaqHe9shZf&rzm|G)4pRjaXm9)
zYYOxJ8=BVnR_s)dVuqDxGue~mCXXq~`)?of=B(e=-!)$&wVyRBDnUUQ1Bscyqnz5N
zs+Wh07wlD8^(DCC5>Q9(AL#EUrp8V*d@L?j=*?0jn!JoTovcSO3eordj2AvXVwGvh
zG$+epM)61sAa-MJ&y2KR8tq^+;?}~rcsd11we{0f_ku?H4T*7Rz$LVQ2GQWdQ8I2MpH>kTC;>vXv2>%x|T2b`Tz
z^SLPFMDxcfe~D6%>{Z%w9hlX(@oJ-P%Fe?e+|ZH2c9hg!;3jy(aO``
z7?^`FjStmX=_Uv&F2B#hX$$qSTnM@?i`sY5X_r1;R=pJs>L@dc6AceSZ*Vo`K}zeVPzwlTVUfw+FJ$I_sX$GkURFDPbHi#f}+YmU_n
zbh>2mmnJ+`R#z7&u}N91UkEP!<QU3B&PYkMNcpc!U|k86QGzcnot>Mxj%rrV&RhAFFpH~|t&~%H*sQ%!
z`VUL1pdn!9xwlV|0>{XjdA0wbnXkp*m^v?=GS<7UKQZIKu`c*7I=gGmthGcxB`tHp
zTugt|wclU;$ZZ->rRj0lUi~O-f8g$$b~KohL2y@22V_QSWi
zT{*3$E?-W=)Yu_=NM=EuHnq&X*qE7*%nRI^vD(ebOI)rwu=a06
z!vYLoovpzA1=t6(2OC72^A^~=Q=c&Ck7&Bhe0H0Z#>Gjn9L!_7Ti)$I)w1K$vz$^|
zRw>o_eN6vbbV8!yMI(-W&+Vi8@$SV{Wy=NoDPbw@A(P;YkgG^$!_sr(PG@g>KlTa|
z2NH&#j_;TQjR6y9*pFqsd$4)3o5a(6jIn`kVDd8YY9WIA%Gd6a_G9qQKA&$U*_^D3
zZX)@H#gs~fH1`OR={phJ$(@qye1aU+w``kZw4_u-{Nw@M=(NQ1g@v+uU1x?bcJbPM
zf!H0`uP&J885kANt;e#8z4%l6s7FTHV5QtV?r6{g>d{BPcPQjpr~~(Mp9m6JgbbaV
zZZ|?;%4t{%CkhAnS|li3#PUfM<&6G&K9#TdPjD>U)tF;cj~}(mKHA=Z@X*n0jPdp5
zW(4Mi%?9u^(wn)!6nq@3gN=lb+vzH?@-~sPWnu!fZfr#gGuQHFEcWZ6BXv6oAcd{V
zmVb9CyyEl1ef(%YwGQ{njd*ZXBKQQh%J(EN!u;AZxncy=>>4ZNVT~+Kj?q2eUbwQq
zwD&H3AH9pez@L}j;=dfh{eJL4s*PEeo)>>YjX`ZYIm$lK#(L>)9P41bWxfgYr`N``
z=~9^NDE;
z=kI@-9RQ*Y_RGIN!yA)^m|o2d8Ub;uoLCZm(WAkmp@@ccK_l^qDx;H$6riPla{|dB
zwa`c`C>1J1sHy$apaaVuGI-z$GWHxe;)dVMC80ovMZ4*z-3mrZ-2Q5-T_H%QMt26@
zuiz4x`DL6Ui4VWM=Ogs7dhG%kB
zn&Z%y9=YN&nZ4o9*!3IC1CqsoHM8XH@s;y+=+zL&`V5h7qz!qo~dh7=9BC!n@Gx
znYa6OPmb{Pj?`OkCWkPr0)2pz69_39#i4-pQX`ZPuHwq5IX(&f(o-N(p$O=VhlQbg
zUOTItM^+h4KE2Jxq1PR?->cw0fg2i5F#%tp*W!w1z2z`B?eAwTTh--1;`nU$xmg8{
za&%QN@@S{Y$2|^OO~C?X%fhJEXf3jf)yk6|j&T}xbj)p=5j`M3Yut42eC0ocjYAS{
zXn{wf5!X!kcX;={>RvQXBwme7g=sf!$;6&E_V~>jL2rvvZVpR-%)9?NBnpDpCQ=Ek
z8o2x-(UZA5%xm$#8@aRGky;uyHO>)F&m6+fh{?b(Q_xbvnoU6=stTJo2Us;WnHN&)IiAX>
zJ*}!(2Dhc4Jyt3{X}(4ccHHfZZk<45oq8;o
zdZWNh>&%$$-$l1zHP08R1}Uxvf2jbk3%`76l}mhn>N1Lu>bV_AseiZia=h|TG{?+|p1xqoGgDH^!2vaOpjaT$QlCzZvmyprCmR+h
zC`7Z=V0$%tZF@RZhfB;Wp01v@h#1x=<&%_gl&O3Ym&{w~x%uh#+Hh^1V>;p5p-a!c
z+9uz@N>5NJ)5OXxXLxh>q*VD_UDLYcX*oo8QxZXVBNtpYzpI=*eT)#J5UTt_{Zm6&
zD!4blPKc3m*pfxVVi<_kuv=I0qr6Od%RkD}O=jKcJQ|$l_`#RAP9uW`P;$3{RPTRD
z5PZ^PA*6YakU=r+pK`Joim=1QFu(2{LP;dVt=*@GGlbX=60hf>fUeM
zB(;-u!k+xfnws`7)xMsQQBYv@`xyWJSt&-bsvH%<$ES9=%;VfrgvM98rD0|5Wb<@!
zH9PRK*5dx9Q@-Z#i23TsF~)Fc6A*bNphOTu8{D^^S4zNv!h<3O!Mer3{vLp>?*L>H
z&>;)UfS}OoYcdLClF4!jXv!RByl9;|2pPV@c6G~og5Qf5HhAr{v&ve>sK5lUv93g2
zSf>Bn!BpJic0}{KY5*~HU5avS8k~oaeQWSgRy8}HjH%*1SZ%dd2+*iS;~t7XV)mg%
zl33#rSW2gq(bLSnUKFSK4Hx*q##34ny&-1`MpIH9GUEn9PEQa*4N02CQ5u6W@6qG|-x~?ys)4%w|aT9cmL_U&NwUXCQop$Nw%VqAnh3iO;dD`FI$k
z)GY-*uu}>azB_D%Ov(!%7kCwpNZZ5;+>DRfGq(`V(4Lqax24ZsX4!^aJU9BI9TdVZ
zbmbw+jphGoS|3q$2n!!*@%CzeMUlW=bLWnWZ3*m%t3qt%0t&nRu%Wu4S{|woj?QJ)
z@Is8U#$JO}7;*eG-%IREI^CEzt*bA`Y}$*dUxz(ck>ygw<@Xtn1osDZm9M&m01f_4
zt$Z3{t!QwNnK68z=HlpWEbs2_URw9r5x)Lr*DBM_r(ovVM21!jiYmO9lEhyO+lJU)
zi`5>tGq_k!)uaJ%Jim6C5E>?|G2+Qb%;1g^d{b=q-zk+KHnsDC^1V4MChZ}D52mIf
z(rs&Ws*m?|H)8RkrF707ApKfwr=Z;=x8Wol;^5;cSzn#=$~v-iu8l_>vKY5_=wrpO
zKV$$Vn~lUHxWi854(j)mROXPo<=g*1_^5wZln}j^WQnE1lCf>m>n+ydE7{h
z@BgW(VXFr!z#^7ocPMz|$foZ-pe&;R$k|Se9?}vOJ)c)EHgfoE*>c$!eS_m2$+P(z
zXaP)YM+cO3W;U7@f|`YM%J(+1THXfV?d?OFOeM_rO-qV1hQl6JXXb-GzG&0ls(N@;
zt2e&+Iqy*{rJgH|E5Pp0mbIJXujNOduN--N4ZhUwS>x_Y4^G{B{K@rP@7_o8?&Hr*
zS5a>o?^15Pw?SZ?b`QsMr#zxLJ|kb&-NK}3)f?)(!WQzvYs&p)WHwjmPUXzKB@>EG
zNqQIxaE@<&wqagg$~1=M1ha
zH=|!#{FfBP@vdlrpna^ecCr1rr3_x4sAY947o*q2lz97f$e}bl^J~UdBHG7G$rZQF
zW^EvE(-Weq?qi>^Do*EKiEOnNONHz1{~Ni8%l5b5BW3y+Ud-ipTw`-dBb?eZ1zbTgCBS>kQ;K{8p>)m979$d
zTMkS>W$U+)0R-J8U4GLecd`zLv-bYDoov@d=Q7RQiV7fl|7ktSy*$ES@A8^0@mcY9~!fM
zl_TB1CT*0P8Ot+ZRl=B2MG}F)eVC&)c6Ac@Dz%mp@uSS9#0tKJ1!uR{BA>Ituv*p+
z6&M8ey^>7cTu^fay|xtx42(hyR9#mW*fs#l8y3)Y_Z^a!elED?@0VD6(w4dAgF$?sUH~y?&j#2(brgw9NIwxf6;QHQb|`QWNm=
zyS2P`e0KR{?1&T5R=a&XW&iCW-CkWm(%OT
za~B1!!uXYL_4`8+uF*GX+f_VzAGN@+*M_jE!3T{ldH!}1E-t1rCxbz`QB_gf5LSq}
zhG8iqbc
zj^Q;mti?F-Ts)0+i4G!f2~8^8Y6{-))a@LHr!q|1CV7Sx6h%w#3`kdH
zLmhi*??5ZIbco_)3(LlSq-d4VFGdgBi??N=s`{p;DrI1Ey$Y+G(n5JmwY7IkU7bK`
z;c=*?1D$g1_S35|aO5N5dy7Z0ZYMq;xre|i18-kqVY%Xg5<9uIUUCg^n$$V=W?IZy
z>jYD5!#Z$~b6xeMELw47VSlrSxTw@IZPvl+Ex>Ul21cW3kNOikPvBC!qWvjU4+96q
z#p!bQF(qO)d0dhtrM_!A$8o&Hi_&rc=7gF=+=4kN#i?h<2InJ7RF^4P)QzUG}xr;C~3amo-~*^SG_M4RbbbDq}10%
z*h#AKuevb#nM7
zfr~5CwxObGq4glDZ&tsuCNIoDXhD1vV9Rw0%K#xGBR07X&Nn7@E>{s;_evJ{o;b??XcV;uHND_Nm
z30b6OSAWnh8dpT>dH>D(EP=m?Ew({^j
z_Ba%~0rBd{daRCOtE*g6qwbZ-LeQ=@DIXS5@{_B@b_nRqr=MC5S%V}to$1v<#?f^#&rSdi96uDrqV&eD~&(w1%`70YX->kHi%=48}FN
zUa9&UZgR2f^K
zqvDPc&-q;@GaNX$k583tu}*XFl_Ar&1U>zsuL_d_-jUUD}#^Gv@?baXmrSyGp}r9A!1AiNS=Va_m6mEfP0#Mh*BG
z$8O9vm@&N5PSj-x$8NvCqoBZKdVY#21^0Rzn~6oO{M0*IjT9jLMlsA!V_LDoqNzGB
zynIoKMco5Rj$qoh;!)k8bJ4a?)%0{X+VNw#JAmlrN7piUC8Ao(T;g(S6<74gUfZ@q
z>QO45b&#@}L~_UG&NI)c`}!wW*CpRB;~G2Cy*hQ3^m6)g@-pp%;{_p?5i3Mx)AD2E
zwnxX~^WaY9TCq-+yk_;!E%=o1<+f$_ajlux#{T+AM^0@U_b9vuA3@(bAAx2s(uv=C
z;3;*>;mgoDybqeObJxsoQr&R5YpIxZqV+^EV$F;Ok!uD|YATaR6E+hTju`7!)=$ls
zug$Mduj==>_YLqixpRw~eLITs%xyCkO?qbi`ofiL%-pZb)2awDCN99G?D$}_0YN3D
ziX;zpawR;zsh6+yes7pH(QQPg33A;*bEa$)Uv&j`*>d%G*)RSb#buw>gW`W*gqmQnUvR$*WNa3ycAoX4<3!UmcEehAj)!4U8x>5CQE(Q$^+HJ+HH^>Pt>A8
z%JedIAK4s2!eWtK=Wh|44=KrtsXplF{!>?k2341&)7Dt
zGrh_%mCk5iI+3hh2hP>!1+(SVO9c%0M6eQbD5t+H@geUDqL+RbetrZ?fb3gCqPz0D
zVJT}YMYSt76MPMowSKBcSD87>ze%Sx%I794+eygH%nxscagM~0_$Vp=&IHmN+V%rN
zGYNy~rDCG1rIVy5qWimT_Z?oTc@c&UB^7K7NF>%gDK)DbWgNZomo!uBuiC71##GEr
zMqfFaSt|O9n^A);ty57g%tGm{I>(cnh?y@Hj$GPQQ;s?l(h@nfhq^Y>)UCiF+iyjY
zPQ8uY+hIT=?wsKGgW;l)u
z-fa%j`3)q7MFzZy#>jZDr-mmHQi)&yb7~29ilgk@+gf^e41li$=I=Uefp}nd2lE0w
zJzTHkV6D`O?4!KHmGak~IU3|`-35#qW;(IPjSGVRZb$}^+|6JtbY(Z1_kPHA>8}ml
z^rs*qn_b^{g5~MHv~88At>-TEcuG^u37OPHsk;#lIiwa5Kq(rFC8}C^SJM+hC9G9K
z2WOuOQ|8C;G+?{R*^;*r3u|TzQ
z_dIzg3qN@NF`zL)YY>EzlvzD~4a+<`(Nv<37TgtOl0pm^rIVb&hDFhbJt|4^ZUn_AMkj&vk)e+2wrcvSJ{LZaJO9$xMB~
zkSwX$wv*XK_m^SptVZ)u@9@%TnuB^V^9k-xMU}idG@Oq1xmmD*Wsj5a
zC+W4tl;GTJC)S+Y#Y=?81zXf1R7qHs2_YUYm9)|*PK;qZk*s5#0dQmV37ILr^H(pI
zp10bR^dW;bowBtMR<|u)s!}UI7XGb^`9t$mCYmV|
zPsJ6t)0OzjK7H@&1(R=n*e!3>mS<|`4P1gCHbJ96|0dgh?z1PH(tWUXyDccKK5QOO
zo|rUYLX_gIhwcB>$8`oZp{!99q}PD72!vh}Isrta2_k}!fV3b*LX$v%7>a<9h!g=s
zFCqwDkgAt1RWKmEDToM$P`m-93Ph0h@ZOm_zBkUB{j>Yc&d%=4IcL6azS;A*F0ub`
zpiv<0z4P*vXLU41;bWD7MAG$R&dpT!4|8@mqzOnR$7*&9ORc5w2Ma!|aQM1!tmW6-?O5
zJAwXm*Dk&0II-{WTkCT1)yXVGrfmkS0Rob|PblWWr<1*5-%wbj>Ov|X7OqKvJ*xZq
zm-Gf?okqG=eRB)&@v4zRH&ExXRok_%hs-+NeEF}7LleZi89H46i7IJWMD+%-n$l;>
z-kYU|B!OmQr-`}hz+;cwM!TH~
zTUw=D7Z)$(Kakl>%DtDe@RodYbWu$ti_-L^)()%LJ>G9$nbp7d*o&f@eFiDdqGek
z9)It&bPaSx1%ZA#U%YE0=PRD%g=0FgltG%vZ@1rCr0jHw!*GRBvaI2a~*n78>^))l)24hHI8>h
z*SJs9EAT}}#}ctd0fPa#jjCd-gqk?2Z2W1W3b^G=Rc5@d-Z4!ML-HiGh2%*~&UT0G
z=0!X+#htg9rc-==(#!m=20Z&@V@473<&>^&ROXb1GmaY&c~fZMUdaKT%=Y<@kpzpW
zTQp+mbNo{;r2Vj&1uY9(mU$ao%|GDOB&HGBfj=~^0~>^BGBv{rc`7VqvpLXRQst#=1S#~Ju1c5#=4$F6YKY|Z
znOS&bdKTSt;q>CCs#`k82W#8u5r+=p2Tu!F9hvi$EsSA7Wl7m`+?qgS3Igomukr+k
zU=O&Ai|?w3a(V+g@)5p$%4Yl=Dw!!a3XtR%
ztm;-2JZPK;V2>2%{$v?lB=3Wf&&m&^d2(JMtoimu-ZnfhV_A0l%dkC`U1*n~99m5N
z3-{!~-Qhy|VC%;6!6|}Qg1|--c?D>HFEWQIZ&Z`TAYOa!LN{H8-)_0@Rc{{2MfRsq
zLFj#)
zc!QJpB-RNL1Q;M6AWimuB%Ler&@u@Y=j$u7l~Wz_vUx(%10|8)Rdo2CZ{9VfX2wi*
zSAO5I&R~`+cdgkj^BKciyE=4g^&}W6H^uPuO7^D4WZX&X(2;UO5*%VMF_l5`27#$A
z`aKR0B-8n%<(@UWST~zk#mv|**{C>tuDKhZH;rSo!Ic8W8)l?SLmn?58T!tqJ@aLo
zrY5hlO|AJUPm=^2s-!+N=$NGa<=3yFmURZ`GW`nJHfb`>K--$|r>zj=cFV;jIoRyN
zt<*u@w?BIO9Qn|aqlt-TgIo$tP2&6#j*I`?9vD{QmUZk3~J;)EFH&b3S;jr@eC
zu{DtwrR%GgCNl6t+>mYxgyPT&`IEQduc@5=GGz*`{&7AuhUImQ_i%&?c4JFYSin~8$TX?wj|YOg$PR_{!V1z|41DZx*j}Ks78h5q##9ihiy63{J0I`@X$U9=5~Z=3jaP+Caf#6T4u3Ry6?4qk!8?p_IE0-@r#Q8Hplx%
z+ON6!z%eLhMT--0{wd3WK^Tw*^j{YuO;wHmNkzR<{+iXF%@*l>Z+(IH{7V2zynV$
zNhc&rdcV~!Nq;-ad892Vds&VvEpbEd+x%;m=OW3OIP>;eX~htDhV+lYeH`f>pJFyN
zxL$nOT#CfKr4zi@J{8)=W9mW0RUAZ}2?BF8HYlKSZ1$tyu1AzS@XbLQNO0ZnB=9>h
zR^8t-V65-bUZwPf8$6X8rMadwM6<=6GzLY%NoN~`=Au7{q|iLa3nUYjL+-hSunMu!
zstGZ3SyX53;3wP!Nb4aB`odo%$>ufsPT^1MoG<1Nc!KY+?npeTW+Veq~@sJ=~Vh+a
zifzUvUb1>fI%B4rDJpg{l8>tQJ;xv)w@nN-O`+c5>*mPxbJ_Yt7ijRbt;1
zvHa*G#(RUbR-SfCWXab-qmkEp=Q$WPppl;xsJNTG5a7>YN1V%3hW-hA;>z`^0BWV-9qY(McERLf>^+6;3@c+pE&lD4#O-=h
zm=JOBV7LEzi+}QbbZ%HDGh4M>$&R1DmbYEXRAp1F5CwoJi=QV9*Yia32ozstS$+!a
zr7MKLWw<6WWz4%+ZY}Y7UGy_{;Kqf{O1GuTrHJnL+Ic*_yaKRcl6ZLqt(_+^SU21@
z{Pj1Ilb=u{LuNZ`nc_HE<#pBA2>Ol=uYZ<=lj)YZie>0c)Rs$C0VR;K=E?e3Yq6Uy
zF1yDC@%mBGr;LG&JYd=qrEosvwMOASNX6PjbmXp)z%8UF_?=)ooc
literal 0
HcmV?d00001
diff --git a/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_incorrect_example.drawio b/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_incorrect_example.drawio
new file mode 100644
index 0000000..e129cdd
--- /dev/null
+++ b/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_incorrect_example.drawio
@@ -0,0 +1,48 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_incorrect_example.pdf b/src/fundamentals-of-ai-and-kr/module2/img/_sldnf_incorrect_example.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..01d4d9e31326b1518381b59cb6832851a9f0cc5d
GIT binary patch
literal 18211
zcma&NWo%sA7G@jUF~k_h6f?!l%*@Qp%*>22Gc!|}nHkE=Y{$${X2#CB@4W8YQmfTl
zQ=`@%`n3PdDwVYMnk4eVqBIP&Y_KE&e=k^A1_lCp0y{%XSZ;1uI%yMIGiP%K0!9`#
zR(e=EQ44El6Gs9%QELNd6JZl0J7bgoKSRL4%+AgR%gYPvx6EJWzs~c_!HF)upT%gFb-04LRjHEo
zkqDqtFSRSYmx-x+(!wQ#{Avl}6FgaTKxGqH}GGV>I9Y@dFl1WbrtRLndt53$D>$3mob}lFr
zRDRk!kV2>Ct?jx~8aWgFI6e@kzckj{`(XZqLCxnjDT0A%!xXkZ9_P9-RxJV-^T%%n
z{#lObv)Bnkdm;NK!vpMwAhGj^hTTm<=rfR-s0+~r=;oH)LyDKTMc9*ccxm7o;WJ}<7Ju|!GRYY?m!KY!Wsv50{a_)%Y!-7BgXk>{1>kSA4s(KxC6iF
zCmv>dq<9OLZ$A3$=bM)adIai#nc5Z`8R*Je3zS-dnmE#GC#%MT^cY;zGDP=g8uD>O
z(Ic>$w1;E7VQay4GFsH5HElMM408b4sO)%rpD-IoB;hGhiqge-!sMk{nEG^2)y2b`
z*&?r5a)W3^?p|oig^xM*MRGJ_YG0gv_J|AlkT~~oQ)=jEES6;7m-b@R&W6Y4Z^=&D
za#DPQ-LM4(8NWFXB9ZJ-3Ap*&Lbmk`@I65=(uwI8d3Z0L=~w(>>q?4ZYUD_XlBz{T
zBHLq>$!|z-z+HNKGS-$`MHL4kgdwvS-s|~qR{GOcmYnp$0g_D>!m#2R642+FGh|95
z|J*8+M@~WX%qoj6s!x|LJ&>Mx$(4_fyUk)9tFhf!eyn3@^OX|1Av<;u)WLanLV5CJ
zeGc5?3shziF-HIiSTj?I7hic!bQQc0fgg!hKu7gy;gu3`
zz3o&B&Z9}8h!Hl+-W21h1
z-UaE@l1ZCiajbe=7`-Ia(_a~lH&DJI^O`qXI*;4h4a|nf=*V%k@*7a^iFVjN5F-L1
z{^=Q^P1R0-_UzPB6SrfMdBk)YL7LHQ&Ux3#LHcm>7t&tKmjQaVX84*?F5(TJSNyCQ
zKPJ0#GBtW$^H}3GcO^AuvqCbbGeVsz);%@rNzighwaQd*LI<9jdL|^FaJtmMzjOE&
zFBNx*pttAX83QKB^1)ty*w9Aj)u9$MoiqtwrmLxO7Y%JKd-n0c_@syDynS7+Igxq6
zw(7q?nK3e&=U%f~^Qu+bQ+Q-0-BVQO&FsZXuHR?dw+lwd2wO8VOi2mH^nzJ7GCv?x
z9W7T+T=?Z8zAVuq(Xp@PoO-roV7fHl052MutiPN!W?Cn(
zT3L>G=SFOLYBGE3!#wy?vo^`4ZhTd46}>t0UBXi#rz*4PRa&cDN2Id@F)B4Sq6`to
z)W{dVw2Ik(%`b2er?D$gWVQ!iqEy1_K(bARSEyTh^A{gMPhn<-7q>3vXN7B%YizU5
zdf~eO7mTl~`!B+bi1-`?zCFc>KXS*q_C5id#dK-8EVZ{Qu`5;Qx(`$j?CVnxwXI2{
zJe091cJaAO4B6!!GLMRX@OtPr@%f5atUzlFcXot263Yfn8)8U?LpU7SXB*?NUcu1i4Rc=Ubif?RgQriVLNZPl~mVsQmErZaFVXnNI-q{Zr
zI~s?*KxqM~>A>zRXdg`}jQq(|g9*Rj6g`^i%$XoPfkUP{YM=?9kE~ujY6`G&Vu+{}
zSbu%2f~_@RYwT9{y6RUSyQ=m>NGfp7+@ie^{?;S*uHdfuj?AO^Ev-|>SIbu`6_8ny
z8Km+Qcj3Tu0t(@rKij(CdKjF^7IGUdc6aC$VzTsDgRv=i2yT{IFMUVLIQz|m16Se4
zsoDCiq6DAm9!qsQGwlrN#Hf;xXDKrqt@cYMaLQOszo@29{WEGK^bEN&i%gxb8r14q
zzg5e|@N!xIelGMtGq9TsuK1INS4opnhmwbyhYXak>sX#e_R5gcbn_$Xt<`e##vRToi-1G+$4Je%etj_S!*a|>F@=_L4b!^+8A2~JOO&u>;O7@n-Snhwy7
zZg6)+cvX1eJbCex1i)@X3S+Znqo!QQ$xb|wM-rZikRwh#srmX>A0m<3DLa&-a4^a|
zJxjilqgBD<>%<9ZzCylPiyLHIS;94gY^kkEiR<5uYMBBx{e~1b&?^+5y|(@vX~LIv
z(l3B!#fm}8KUGbI*=h!tnT0jW9R|@D;#4P)d*}nuA({i^5c7HkdX>3=+;Y2x*xA@Q
zj5D7XoGux=CEU5L8ZV{C&I{j-*t`ytcKB?Ok1r1mYTZ)Z0v8FTqY7>CR&yk0MK#4e
zlDU$8Ne_}-#bQPG)FG-L0$v&&QdWznjSQNe+<2di-Bcg$Z>87kyL>T^gB^R>LUedu
zpDXLbp0PZ=F^Hhw@16l&SfA)#y^w3%AZ8Hx-6UY6U~y>61bcQ^5G&BP3$eo!?(o1j
z$_AS{i&DlAcIZTkGYokx=nd>CZ+QUvxM&`sVFxWc6xR~p^j95LYVQ(nFc+rNK`-L>
zp|IQ#4vxfM>L*0!jdXKHYdkkNSI1~$H*t4Rx4_FnBK7p!T0WU#zJ}{N3~jl&L?Jh!
zwSkaO0+-$^7$1wLwl^Af#2Ey|hRtd?qe&zQopVx9)Dvc{Me3aYg;0i2QO*+U;~htX
z*<{x28l%tH{_#`$ngh$C(Xg_LYEo=O@VH=cU&3y@NI*ZhU-$HxLx<@8!J)C4i7ER$
zuIrGgOhZwIlC)@$E}2x6Wac{xXICA+nKZ_gTn6gy;|HX;y1k;H*+gW~x6+hw4=xdg
zO8|*VlJ-k>f@MLGXXh`a&L(AS%6rz=uDT5wUpu}`wnBvK%#1hC=86DvF6nN&f2+hm
z^mHiJ=HdB)%;wLtJJw;+N}cZfwuWzSo=TI^A3%~rd5ZfCC1e>9>Xd`a3lojK^e}Oa
zNtP~lv!Z;JI&D8CC+gv?!OZW8aG4m?F-=qER<>ie&uc=(3`?yeJ@ld`3)Dz9RYhT8;%8N94-~
zkorxDeWe|`0vGzQ=SGJIN=iPp)3X{9%>u7?yD631oAuT}m#UpG^xg|=A(kK(gQ&LY
zVYB-X-(>V%(j}%s8i&i`-yS|iAweJpK;qFk&eUkyfRks4Q;gc>ozXKdMNY5rpme~V
zA1et{mxqT;l*tFis??8XC9~(!skG%oo6VVYoOM8hT$|K>EKg2q)X*IE`aU-WX5x);
zd}Olw;dTF8$>fiDwB2a})tg=4!f#RvMf8`!X>%MD0U*=dOTEg48r;JsVfzBj`t-Vt
zZNTH6Y#U#(M+yQXRwbOclG*fnZJ)R0d?~b1O24`!p{fXV6}>6i^<96r^jTIOn<f&L^}Bso5w1>`;}nuEvzNJ#xsX0ZC2cZk
z&8TV7W#{}o)Puo^5W^0|oHB~yH$z958T!M)iU-`eVDlckW8P(xKN~;b{c>F&#ZTjR
zT~@!fqNU6*`6{{rz9BWkQ?=cjG{6tJgYY-txScuWz|T7gQUzW+ev(t0zPNm=cGSft=eR5xYkERu38{{
z(-R_1zmC;SNgw=aa>ggOA@NCXp>Hu4LjGIP-;@zTi2}`>5N^uU0=x>`rq@m)pE)nv
znje~?*Lj<5{}&g%kUl9#V+}=QR3M+?1vI~NEzNT?Aw>H=>NjJH9|RbK#!a^5>GnR`sJG7P)||0{Sm?=U?Y
z7%}q?cGxF2%2Gpp$mB0n6lJ(2l$4M$=>W2ff$I
z0rL(?<^Gh>P)qYaK~9$6SHz71WRwxCp?sn2dZ5_jfna0`G_njNK}{t(Z~x9-cCL(t7}|
zCXdY>+5o_HkLgWjMslak&PV81I$RMk1MdI`z51)pdT(2ve$A1CYkb^sq5G=KAL(xe
zsVg4Y#J4-x{nfp$SIQjl0R7ZH?w|UtGfUO{a+Z@5yH!^oDI20QP}TC)K4s6HBpa?X
zVru?j7iaJq>l9p9s-n^Dgfn1y-f|nN{fj$Y(K+lFqG@rr?hyeKsb
z@GCfK1l{F=e@ah7AkD~bhu#G~Q2Pk?K>12{_~(9UnJv8|x}v+o-Zr~SVCB!9w+nzi
zG1=BTLE9$uR5>dhxWl@#1MkUOZZbQ*1drVoeutOMv@@5RR|wFX&FuA?@%z#P#VfKk
zqt$D7g1gPIoygwyf%mhNhd+9AvH1hZrv2W}V4f*hW*U{1=l1W?=TpwwGrji2z+ir$
zzeMcAB$HQl<*u&3L=7%em)P1fy7pu*Sf=KkjFpGdx}DP6v#a*xzQ2SGCUcYA+Ox3s
zMCR|!`+CXe-}>AvdHlP?Z#fY)n4kO{EGhk#nL}#rx%RnM@|k-x|LKyc`^(xhzV?Lp
zw+tORYnS@UU4q~G-T$h-lFKLj)jPG1t+l(&wwxDE+(LSC@B|TRSWB=;XqUjvF9?B%
z0n+<2DH||rSrfB~VoT)k5hHI_NebKEGuzi4(Rq`3G;tMaBlN_+}2g_c?E
z0+|Aw$~+Ek;zicdn>Jvh#`7oPY?`qpr?cOAGD?oN1`=Wkb>e%9X=l*?fS^x$-?5nk
z=UWy6Yn5hN@{AfGb~67yw4qt)V|WR(VGPi%`hgYIElSl>qAJf;28{{2+R2!k|pnwAOTW(PbD4y*rs)9bLZc
z;XGwDB5y8C-fZ|wnULjQ0~Luo9;5aijNCk!Q<5Qji3U21l`Z^!C{|rD>ybvm0`CQJMi{rPkm!U_<;|0(OCl=83Xm((B)ZJN9de
z+E!S3w!PG^CKHk1x^w-<$+mC8w_isoC^GrA_!(woXEJZdd?*m@x+wL2FFK)J*P;~(
zRdp!9h2S@S8|)eMW?S0XP`7a_Jl`PqVjJ6x29Q4M>~~82Sejl}=d-)5xdcax!$1WC
z5WG{k)ptr|#DZ3dx9D8%XdZ&=;9qM0Q!@|mH(cBIG28cu?p;A^mw69dW$!WDF1xZR
zNB5(VJnuI(uUH;e{i<7ru~oiFe_$S>)g_{jD^TbHM0L5-&@Z4m8}1?AcEbV6`a+FOJ$*;+$6mW_fdf(;`<+!nAyIM81fySNnAV
zYp>?t0nW?>PR&0_6pRJ~XUx|#{LAxo&S{YI;o%uJF~0uh=Eyjg8M+#qZg+i+yRNf=
zR|PM?HHQBza-Z81;};=Qjh%8^S;{h-fgvOKtAbr>Ls7DzYRDZ4dV!cL5w&Pq4m^*~
z1=RGHiqtiFxL_CKK65R4W%Q^TNFk#>ZY_Fl^spv<5%pRkYIQO6N@6&u`9K%rRZAE4
z1>ck8?!bu2^`g|1xVw5zv746_(|5wIMh!P{GMf~n(K*wTxL+Xpb9zZUp#}P_8Iu+B
z8LudXJ#V8_he8GXRKJ;P8Zi_f3hs0hio50ph*aV?MG%)EVvyrtEg?^e+=@Fy(nE`R7LeB95{h}|
zIOM5g?_RqlGfRENU%H&zTm5jCty*=5?qRD_8S+>KY9e&I0-JjTv0%Kg=C}kl@?`R|
z33x=0RPJmd?>M(|{3**&2FH6Ou?4vJS4v$S&wmwoCSbC2n*pD+X?ssYpaq6yb7U*sI58lW09g+W0j
za1=NN;S!#7kcXDnAdux3y{!lF!SWvj`XM|m`~L%&f6cZY@xR93FM46Iq5`l?kOu{B
zNsuQB0|N(U00Se${}a4l@E?5t9^zm759q%J6B1DW1NeUuk%+;4eDEIzS4eOlL4ltH
zPe}g(>_^ZxAIv`>|JMY5=KX8_>i-U&6`QDw#|GjJ?`qP~fYU(HfYG2m-wI^sLFWA?
zI)I-^&qJKiATpsXLs&q}AX79AFbz8Nm&H)(iJA(@A`z6u*moBA2j4h!;^ra$0m;8c
zKsNPX^H=|O@Rrc5`wnI@h`O3Ol0Q;FieF0P!&{!r9LzjloCCs{v<$*IMLZqO5~3;S
zFg!^kZ}r|@nb4v;ZUJ0^CXQJ|+%ljD{XZZCKqhDs{Da_sjkqQ9zlH$t{{`>LARRS>
zv&i=s_(OtMh-M6De#|Jwv*9m%)BK`It~m82``hW4Y!b!8z%_nQo(GW$x;d*k;<0nx
zMT$ar9CAn$y>T!hG4(%y$21s$f%^wSqCXk?1^>Z6iQ4~)!3zSt1c3y`e?R{M7BeW0
z0p=f&|7!$+dH#3ru%f$Z3*0n=bsS52&ghXq!KQ&9uwPw&~gym_-!70Jf0&fI#CLAubm8XLIGt#nHN{=%RnddCi*0-D`T+AwPnNeWsg9zG}9H677xp~_9Df!ab#?>$%}E0w1$^=29d)pj+q#B(xX
z{{HzimQFpEktK;!$P`UT$VtepE=)r$!0wf7VX?Vjv57=w1_EVBfHGivCE$Ccu?~sj
z$IKkk5u=v%X%nQ0qxy5{zfjV%-q(Dal0N6AE#%$xXB-y7TZtU@`3m>8BK1kbOXQDO
z0f@GOIyKCsDYSCQB~zCAN=955vkSjBS7tRnd`)v0=t>^hYSWA;WwJNEbMtvwQkyL;
ztW;v&uDukutIN$R)A812rSH0$DS1&76ud`$r;`J!3|b{z;|-FL?vZcdVWVWN*)5m?
zfl#GDMa^mRGn4aSP-~>ba=`d`vv0|DQN`_(+9y;P!}KEC!L@wHOUZ-lm^Sug3@32C
zf{gk7i!&*M`);BS(U?h#Zlxx7EH=-isNC<_J+_-WKto*XiNjur=^m-HFcHH#T8GbR
zWpmo0;BZ1bAgxJblW85Qs7!hJ4>LjZk$~4a{}ejK8h2vpk+lF>Y-*6Br~+a;rc6qq
zpl%Foj}omO*7P{qHGu-HUeY*UvG%2~o|96|G@G_*0Xft40;85JO@m0%Y63Me+1QgT
zWg>5icR>`L&-vrn{wJJCgm10%RjyA8^V@u7BA>OtX?@?OgVl2jGuQj16n}Od_7d%M
z%sus;C$u>ZwzO{m(@dNFtRo(+`rI_syHtkZ-kZ$kX1Y~RF22@ygV{@_r-jY!dGlt|
zX+lYN`ssw}XJE-g70q}7l^n9$du{9HaXr3%a}-mgqXrF?AAuLiwCzs4s-p%~TP1pv
z$cUwGUsFv})v_=GDB6s)ze=$jv!a`6dU-Pr;2euVNk5g^MQfKC^ZA{VWd*O{3ER+u
zAP21+Y4MhtoOinZre>S8p?*2~_Q1vniL3$j*ZMocSG1?i(zcV&w{x
z1AvHJ&!^`I!sseO>hArSJi{9Z+He>L*FmM;OcL--;o3FPUo{YkuC5;$aPqt0lEHje
zm{a1xI0E|IIBou)oXWdBql+~2x0e-|7FnmPKar%O?%D?!(-B?<>ZuP(e!7HW9;B7%
zX5eO3;{dW*mAP~{G`VCj%ZtrH@-(Fi@vt4!y2lN#DJREiYMUO?i}Nk}i=e>=g0@|*
z1G#%&N2RU|&+r&bkOpGIZCaJydK=3ydegmBY`N=)(;ddsIPQE%
zpcnxaCuKjU`a#;Pk!Wl+`SgT67J_2Pd|!{G-PI8WW6({-87m~A4tD9~l~95-cccPoOU8SiOybD`4&UWD@z%Nfc_=I52`e{M*fdnDMF
zfQ*fSHglwm4M$#nS-8SZh&alKitgflQS|sytfE+xIM+UHB5l7#4{Htio8Qaxui4+>8@
zn+(KMSsEa!n`EirbgjDHL`-YS$mzuJRT)CsB%+`OUXaJdQdt+0_a_nL5*P
zmsZEJ&lF88j?e9TTnIWNyG}hPZ`ZFPT`n7Zsvo)W7kp4|+#@@QyM{J@*v)8R
z#RQA}9v?v48M99&QAEYWq=-op4ve2O|HVnEiB}b-Dq2B3n^eY;fz>2DPxKH*oPg&b
z%1D$>LqT(xvVblnm7!S_qa3;TgJnfN8Ylgsos*EH5cD{fV=vSjLv2H~~muu2^iAY1euI+%d6C
z@}x61)H^xeineNBcuEmrmgv_vCt4FwjZ9dT9>YS25JyT$3gy@1mZFZMP881?0acfy
zDyk|9@h9*;ijfMBWXCpZG_$Oq*aXHXCb2$t;)Z=3A*UjvF(>_uQNM+bhfo!@lZA4t
zR=D|^6*uW|im^1rCDzHe%Jwl|ZbcaXCOhirmrbQQ|Mt6or+tngIbdwI5RN1SO+F(z
z-GUKQX6a~E;lmiFOflQJ_*7m!si|IeX<*a%b=APsaJtU7z79^mMTmZ%)r@&zI))cb
z5&70SvHI6E%YEAcCRdNwojGU8Y93jq_D*RVjVvS##-
zaL4VDxYjOJJ#tZ6nT_K}kSN(C}
z=1JUxRV|bq7#0&)17AFic`$Mf`pP4p1dTuIPmT3T&x=XeN_#0=!U`
z2q}?j4%VUmq+0m^0qS#}96&T2$us#Bh0BTS!Fj4NNI!*f=pvaO#wa3+Y)h3M{kwsx
zVFQzC^f%OOar&RdLFaev?Z-*6WMWp9zK^CZGR|XSN(FmXtLIM-YYwv%(=y?l^MYJC
z2*n(QO3iZNON-)W!x(j^@@4Jq)ao=tdx|n~!%|i&rmn@xI-07Jz?6g7S~I^VgJvIL
z-!iC{k>K2!YM;CgCEu_J3-}793duWaMc`c_lh~`6m{dWZxrNTL_L<2ND$m3aZi!Ba
zTIc0Y#Gf%StjM^Z_v=@bF70IN^TZ@ZH{m);6A@BCWlbDGwgFqaVnbUNsq(gA>U5u5
zDGezKDjFKs^86dgqaUHWPS}x?Jjs=FrBX75z7`jW-Ota|xoWZwMWVM(6%EzVcT!Hu
zp$e1rqCBEC42DV397ct5WZvQ1jrl<Z#00ko#N7t6*Lok-3%34#Y(3Sj$26P~R|SX{4ha6b_H%Sggx>ZM#i8Neq+F=$O43
zH+HnHX~_Gm(JkQGy_O0WDk18%zukBk-Hsi}dbm0kwLXP6)VObPlvkDz*l26m5=f1X
zc<38>>$+%^Ww@9uqeVM&c(WYLTrZ}rV$(MWa2Cm~oB6Fj+xB%A$l>C1@KHWB9%~)7
z_%@8D@1}}!rL3fKq!?4MYgyBPZ7}+@756+M3{^|&w!82JTONLy-}
zE=&;q7Q)NLr4A2$+Qs+4<5?e?y=A9Oo~hKrQUrzEM4IhHQn;lh?!OR66k43)Sh+%BRRY+s&%_+M9
z3o7_NAa32;hBxvMPN#tG9cBLSs9p($ThG#)cDK$JZx-YG$QNTnbCO4P2$xt7oR5dz
z)=z`a5>s2nbO?TKI8Gk}w@q8DYxJ`O9IEVU#<|&E&1Qg4Rf`6*#7~Cl_YXTqMIF(u
ztPI_4Q_^m7Da*g_u&2jIYt9+EED{hiw&}pKEoLKL=wHvFdh!w%z?NQsT50sjugjl&q?aAe=?_g1N$5qPE~QdfL>b&
z6}g!gw0LKDn0_vMvroL}KDRfYWof7n9~|CC5eIIfD;iaBVjNbIVlm{_#_2U6lji0K
zildxncboM;Z8ksW*Xi?GjzP+OB>-L{T~%F$%{1-}9Wc^WR53^Z;A%?l&Deb;*
zJ#PVT@GTr-8SIa~#sVdDVMXw~|43iZKqeJM)0>)CEqDc2+D0mUQTL#)rh%MoCEB-3
zucz&idtPDVHbPl=@LBubimXrWgDHvR0oXvoM
z`2=7oi4x~E%5@^H(8e`>0#a$lM&f{?vgO~CHJQv9FYQV)4XR=$P}d>Mks6=WirK#;
zoL*N%IC+tpqu^_pcFrf`-!Ur`{YVjskwI2bjtqpJgf2I_5dSEcBfAC#<}JU(v9
z#Vg1qIA}p^@q4q-q!qIip0C|L*HWRUa=6r$FI4obr3TjZ7TFn+WU5!AK5rj^`+z$h
z9dQS_DNzHa@Wo^+HDz`PLl=+ausMMBP9&vSYfvqu;cZPcspo?nSK}+R=Pl@ACuanM
z)U*GSE;VNqNh!#?FoVO~2nh?%g-7$H(yI5}`ownGs+cr1KC@Wck7SQ&D{H65+1aCg
zY{_dW)#lEcdi{J=oAnrznkkmiV_{+zc4+dT(D{kOIXRM~OPsuw%?g
z7`yTp6;+Zc{5{LuMAlqy%@N~)PlsO9s+OFrVL4J`Xbyf@I;;6ycIP*K4Xpy4nnF#S
zmmNQ6dGxgu@{F{?5YOaKy5Kd3(FNW|yOx<);y
zX$CQMT!xc6|5L`+a&-Ds1-B2twBGC*ZL|kf#Li+!(|lX3?v<1a6BzD8lV@5Y;<49a
z+AdsHBB1Zj7Yv%Q_&{D0H%b+@GbR`*8zu0!j@oieoo_YKgaBfsG
zjo!!+6?WvgfMl6+eZkmM>j93PxZJ_EKDCSKWEZdBNyn-UajAu#95f1tm|Eez1V`T=
zg2!#R4?YHM1n)tkDC!c=QRVVl5{qq%6=XTZG5CBYYTbNWD(WN!zJ7hd3Y69ZUu1Re
z@AnFo_OY!*(Na=Upw2Y?P;1Kj1f<$owYNtsV(29QB%y_1p@%FBln#(}qVnb=
zybjhZHsr*=Ab3r@R$g-W=GKwDK5|?hfN-zt?x{|!gw~`u=nf=ef=-|rdB>iq8%479U+9>SpSkczp}Ud9_kZGdQViUU7xIhGo5Bbg9nbBEF*jS~BL
zteN5igI;~-W*g>GFSi
zklJBTh_?db-5lKj{8<*1V=n2yF_fu$^NnIPV5n`oLZMalylrdzs2V7zbsK}tdfoRu
z1auB)y43R+g2vGEylThh?eLzhyy%AG#P@`WS<8R2-mv+Z`$eU`%hG+s>6c%bJGt{O
z$D%p?5hm!OQXjhK2lO87m!hY_xW2^Ful*jI{!_@O45g}~+Y#lfVZA2^hkygf;*!MX
zOeMEJsJ8PHeA_S%nGZhr)XO{^WSP|zFfZC|dWYKkjHcLQK9DPwRU+O=@5nW$Huq!u
zDxJEQzBROmCYyg|JyQ1%5BKG_;nZd73=UQ#cCZ(*$MPJ-XHoY|fA8owlJ9_3{V-cx
zTZ?TqE3`jyR}mX#uH(TEhTZ#8sbQ||aDJPVlX9F#nSnAKmF28Typw7Ml
zns2YT+)Pk|b6aSLo`kl;5E`?`!%+DTOqH-(wKhGra{BY(UZ$`-ea2-4%@j5wW%U${
zyE7><0zNvn_-VLbi_GBn%;);@sBf^pp+~vw4}@%M7*0K{P&3ZxwFR
z<_md^rZ+geOnS;6pH81vYT0T)U!2bN_qUW$CO=O$?!@FP=_gAnQw*LxlXF=Jr?BV_
z`j)XuX@w%PB(n1rC+FRCqQ{;^<}P>V;|F)2=dJ7B9nHjpR=QHI>mEPZYxC~Ms9(c8
zs|lu#D_!~a#X42FFjr`*YgKLi=OSajF*i>U!>%mMWJ#!+OCFd~Pa9sGfrdi1G3nB}
zbQ;2fzrFQ-syWz
zMz+vgaHZtR#ePM0u+Ilscc-$~kj;JMwBlJ{z-sq)Ax~-Rr4suX+kTj}OGF`6I
z7zMpV;KvRd*Bzjqgv2`BxR{fs+FDN5c2L2|lMe*}{v#;`dX-3UJJzJy*Z2f)&
zV`RFsfKdS5d;&`RSZCTR3^bfyftISSg=`3V^)-vip)i4?m>QWQ^39*Bss_r*QTcs2
z3yFPV)F!fo}ChrSlYYd926qC_V3c2TqQ
zo!!s!4c1n+7Af45l^XXLs;m`-6&a5Ui;GzG3!U;NOCqpK>%O_t-Q=>tUXGI@yk_N+
zZ#x3-cLZ!154Oc(t3`uJ*<-##dHb@gyi}9P3oYSJF!XceL(U
zU}3m7v4eyg96ccy(rtW<#)=XzYD-JznAV%0K7iB>vN3x@hW4{ZX8)Lp(@U2q)JSqa
zOk;mECBd^+Rw3O?zgbQm@crS3LrOU!b8xh%%igE73-au889Iez^Pce)TS&PK<9CA{
zuiB}Q?XmDQP+1Jpo6K0OySNWmTPk_2Br!s}OzW?ko950T;=;;X5sf16^Z%h!Z9mrO>@zD(E1hmQ?v5vPkn#jAQ=6&qgh;HuCcoi7?x#?n`AHReOi4l0E}
z7-Fm7oFvGGSoLZDDn8R0Y>{zqaJ^1?*e?|cD8J;kWxtNfXRI+kn69a|kH$H|MZ?!_
zGzzU%QVLdSXMT1zkPr%~VQ67xpF^|t*d}U@G()`V4A_5OjgD`Z>PGHJl9*&W(wZ-%
zpzO7tY^tWOxx%|YjjS@NIs*@~t^uKB=JPqga$kQ~xR=(okyX&T8tQT0vncsyWB^Rd
zWLb1v%3N8bCRN4CXctX6JjOlUp00zYb+U};GZ<`Q%MO$1Hh87VDfqUA@t;@AGI{zQ
znA)HVbFlAtsEXxj4-A?sUA3lz_{7D7!v-@SoW8+0r1yeu+oZ7z+)b9iD+zqyQ|LbYeL2*+B~Pq?Np;hO
zm9<)jozsa85BIgJe-&BJcLx3z5c+yoGnnVxL&9X96W7MFrd`X&QWa7Iqg9<_$C>Km
z`$efv&8$>)>>tx%Q$yW#a;+|#5}RVsx0htlcij5oCmWUK`^LXV-9fQ~TOk+9bmCQ%
zD&Wb#R9vZyQ)YrdiC3?}lZ)Wda
zmAFrCD%T8UqPqsq4@}vMO0M8FiQ&%Pl`&<^CT#99H?3&l&|uzzZgFqtkGPJ^(zG{G
zorJLcTFOeU((7h`Roh+WXc2u%r
z_c$RtCCCVr{x}#x74IZs`3hTAOAs5U)vlzXE%^q|2~E~!)v}UCV|xG_w+1qduOUQxNmCze1Kf$h|`Nl22c|T^k
zyF4hcf>Ske%sZ^IOhidv$eIUda9kmiOA`7iRsU-kn;r-E+qOk*BLJ{SW+U)c9N}(R
zi={Pt+P}X(UZj+pljAp66;G1gVc-^n8~)kZ$;f%2ajZ9w5sIDnn@&0=raB^3dOW7L
zr{>7>xg8mLua0;;_!FJZ^pe!OZP#+6?l-HPOMlBzy9b9>aVFu>&dOXKRLYtfYGsq2
zc3vT9Q+^DM<79nakfZz$rQ3LY78hg2D5FzEJ9L_eH6*^vc5Hv`>)6Z;*mZK@{+XJs
z;?tpJa*Ur}kX_xM(^yO%&5y=L)&=Dy<|@6J$&(R9^bbuX0)7Nm(?-M=EkKKS|pEatE#w#NTXjQ(ByGj|Hh
z!1!MisQZjL?bnYU}{<-w@ac!@xg~{$Z(yRS}*z(`KUPeu!7TjKtZ!ly=8W|2Y%B|loERS)d
z3R<&EzX%z<#wU{;jhao!_D#PTlnxVf*Y9swT>*2R2HZA8ZKtQ+`@gW-_mxLj9q;Ap
zay>2~^r9qHVd37APE?e&sd-N#x`$*XV6#}JX_xl8J$$W1bx`T#9#mndebMt3DmSX}
z{kv)JQHf53vM6|hN3lhCFfHyF)Tm30Mxh{(gt92C^-JPT7!^{S?)Ye~t@WjKy~H%I
z5%V4ux`??@UuKe3{EX&43AIR)f?PZ~!8u_{9fzE}rc_XCbqF0(!`3?e+y>|L+$Za6
z48B;cc6Xh<7on|lq~-I+mt}>br2kVNnEqe;z`^vt^`S|5U2>2g-Y2(aq+#27PTI7j
z_I$wAZ3wzgst@VA+IKbiPkioqRW~#(v_>0qMifWJqoVudr45m&*A@I=#q^`z2|+fl
z$9+jb*}hZ|KWU#-z2wRBk`DeXG2;T$a8~&O+Pc_oG>f@1kF!Ej$KW{1Y4#Bp8<#@6
zmqYyMjDTT3gg=!VgF=rm@uDE0*?QwV>+p6}!>PT0%CJtG#kQFtK^(Ls;pa|>u&D^_
zld!aOvyB<3(I*H%Gq)EE4nPya!Rl1P4@GcH5f5TmY8!0Nd)Ta+#%i(Ub0OT*5ufTd
zMB8wi%||p}!Xd&Xl6JVGLNGLt2}DD7%`TKi@+%i)@%<>%O;mu_6TiZJH?4&Yq2Jeq
zjsGP1)`dV_jNkAz*`ZMX@?7HwToS`OAS`xt%QxUXULrf~mr^dh#Lr_*Xx8x+@%wbZ
zwEzOjfrxiCN6Mwh<^m(Rv4=e61EsT-1I_>`{S}5JOY1;PmmlJNo~KgMr62~U2TnNEzKMa?9FLy+)e+Jls9lRuyG>zXG&bj!qbF+nVF5{pKrnceMp?1@js#e
zIU~NIz9qNM`rY@aruN1k5s(?(uv$y__2la=`-Qnh+v#>WZ2Dj(%h4cU&!pjTrl-q@
z>$Rd*-qYV%{FVON{XG3Lb9&0O#XKZRiTOv9B#xqrEl`|RLZO311(8x17!qX~zUSpz
z6Z9T~;oUzg`yF)WW&87?n>}p5F?bv0I@&?D-Dg?IZi*phR!lVpdjY)sQ8_vb=?1X8K4
zhAJnK$RyW=Cm9-sh6b*yQ1a6_a9d>+2hTrWnWX>}cH!S_UcH4ic;~2g=)pz9Tm|)c
zh|<%{=T*P3h!ZZH_a!yTaj+#1yj^VIH2|35t8rca=mGGNfOuxfLPh?BO?nkB}IQ6e1FP`Q(e~--beT
zL^6|;Y8%8y5`;wrlCy}?mTw6mwufU0Zo@?o?1FeKk>^>#wr^R@o4TuMt{Bj!;Wqcj
z_G3cYdnbEM0JM
zksl&P$I(af@~?Fq(!I&3p7}^hHQ0
z`QKSNWI5|Chmh{k4l@&-&`LHe(oOTd?dD?VzigznxR3N_sY^ctVHf=wXKG2Gza!ET
zIh8Lxym3})S-(onSZXQCqIT3-RBm^6#%Y`?(;uIg9Kf=}*^ft0u0E+9x8bg^1$3n^
z*wDB^TAG@*`QdNvIN?GxDDexXXjSXJNq!6;FISyF%XxkRSi0Vctvs*dN(NHDyZA#?
zOm4>)TzE-Y_r#TXx%~klQC;e8SdrwoHKkmlmmc2#k16k5RCCRnUppYkqcO&Di+H$H
zpViOD=eJ(Uy6^+v1Y`|7T
znIRQXSZjYsx#gdf6RdaqMcE
zP&3KXgR#{q$RkiD*u`qf63^EYlDhu3e7J7t=@`^GA*F$RlDc|d`PU8RPu6bgwY0d`
zzRBVO?|bfDOV;<9uYIrOeMz!+j{39Aw9UDD3#~LKoq1Csev^;;*{t_@zJW88bhq0s
zy}f(kx14)aj`YcJEHC9
zolZY%&GXf~R!Cy&n(oLnUfHwvG#Az!(U{;lq2=Oqa}LL3qiFNB(iYJDMjq_;U5#I3x3kQKy2J
zCytBl{JHA$?T2ejR@liZ%kH&#{Qc(?mV57Se>V-D_FTl`UX{@yeXITP=5y7{v^JeGV!9q+bmdv--<4X5$pKfIx7UZZ-sibErTUzr
zNyE0V|Gtaet(SF678`FUswfSeua|Z@=l_yy?>KvzH8*uv<(JN8o1PXdm-E@d{qdrG
zrXH*NeG{d&eax6pefapB@6nqNOYuGL+1WOgiMKmIf1O8($i|(UU+4W^+Ub9+^jOjI
z%DbydX6N#WES$O_UH8`FBIlBT`hsn$DGOH%P0i3?Z?+3oik<7SkuNcAo4xVVXSE|NaMu`u`&tG~ic
zH?b$HLR6lXwaA|66{m9$3}=xi@c}
z?soQRc3)R&hrBmAu=e8Ff@&MF{MjnGo}Ya$1y?3#UNEo{wp<=ky|rbX!$q!}cV(uU
z&e?eBeZh5&xp&rWTDFvHpKXO#f7?G6m&dzSV9TfGNcj}p0sywg^@H;BOB6uu_aH8P
z&%CsJ1yCCj$i|bABZ5-X;Mo?GgTob~6@W+10AVc1kd)L4pn!pbp#_kSe7;O_Lc)*#
z^E(|I8W~*-nmE)14)Q2PIIw7UBrprUQD|azDKKg(F^KYI5;6-C*c;QcEx$2lIj6&+
kvrUbR3{t<@)?x8gaYTS0GZRfMF0Q*
literal 0
HcmV?d00001
diff --git a/src/fundamentals-of-ai-and-kr/module2/main.tex b/src/fundamentals-of-ai-and-kr/module2/main.tex
index 56cc9c5..810bd74 100644
--- a/src/fundamentals-of-ai-and-kr/module2/main.tex
+++ b/src/fundamentals-of-ai-and-kr/module2/main.tex
@@ -7,6 +7,7 @@
\makenotesfront
\input{sections/_logic.tex}
+ \input{sections/_prolog.tex}
\input{sections/_ontologies.tex}
\input{sections/_descriptive_logic.tex}
\input{sections/_semantic_web.tex}
diff --git a/src/fundamentals-of-ai-and-kr/module2/sections/_prolog.tex b/src/fundamentals-of-ai-and-kr/module2/sections/_prolog.tex
new file mode 100644
index 0000000..b2d764d
--- /dev/null
+++ b/src/fundamentals-of-ai-and-kr/module2/sections/_prolog.tex
@@ -0,0 +1,287 @@
+\chapter{Prolog}
+
+
+It may be useful to first have a look at the "Logic programming" section of
+\href{https://github.com/NotXia/unibo-ai-notes/tree/pdfs/languages-and-algorithms-for-ai/module2}{\texttt{Languages and Algorithms for AI (module 2)}}.
+
+
+\section{Syntax}
+
+\begin{description}
+ \item[Term] \marginnote{Term}
+ Following the first-order logic definition, a term can be a:
+ \begin{itemize}
+ \item Constant (\texttt{lowerCase}).
+ \item Variable (\texttt{UpperCase}).
+ \item Function symbol (\texttt{f(t1, \dots, tn)} with \texttt{t1}, \dots, \texttt{tn} terms).
+ \end{itemize}
+
+ \item[Atomic formula] \marginnote{Atomic formula}
+ An atomic formula has form:
+ \[ \texttt{p(t1, \dots, tn)} \]
+ where \texttt{p} is a predicate symbol and \texttt{t1}, \dots, \texttt{tn} are terms.
+
+ Note: there are no syntactic distinctions between constants, functions and predicates.
+
+ \item[Clause] \marginnote{Horn clause}
+ A Prolog program is a set of horn clauses:
+ \begin{descriptionlist}
+ \item[Fact] \texttt{A.}
+ \item[Rule] \texttt{A :- B1, \dots, Bn.} (\texttt{A} is the head and \texttt{B1, \dots, Bn} the body)
+ \item[Goal] \texttt{:- B1, \dots, Bn.}
+ \end{descriptionlist}
+ where:
+ \begin{itemize}
+ \item \texttt{A}, \texttt{B1}, \dots, \texttt{Bn} are atomic formulas.
+ \item \texttt{,} represents the conjunction ($\land$).
+ \item \texttt{:-} represents the logical implication ($\Leftarrow$).
+ \end{itemize}
+
+ \begin{description}
+ \item[Quantification] \marginnote{Quantification} \phantom{}
+ \begin{description}
+ \item[Facts]
+ Variables appearing in a fact are quantified universally.
+ \[ \texttt{A(X).} \equiv \forall \texttt{X}: \texttt{A(X)} \]
+ \item[Rules]
+ Variables appearing the the body only are quantified existentially.
+ Variables appearing in both the head and the body are quantified universally.
+ \[ \texttt{A(X) :- B(X, Y).} \equiv \forall \texttt{X}, \exists \texttt{Y} : \texttt{A(X)} \Leftarrow \texttt{B(X, Y)} \]
+
+ \item[Goals]
+ Variables are quantified existentially.
+ \[ \texttt{:- B(Y).} \equiv \exists \texttt{Y} : \texttt{B(Y)} \]
+ \end{description}
+ \end{description}
+\end{description}
+
+
+\section{Semantics}
+
+\begin{description}
+ \item[Execution of a program]
+ A computation in Prolog attempts to prove the goal.
+ Given a program $P$ and a goal \texttt{:- p(t1, \dots, tn)},
+ the objective is to find a substitution $\sigma$ such that:
+ \[ P \models [\, \texttt{p(t1, \dots, tn)} \,]\sigma \]
+
+ In practice, it uses two stacks:
+ \begin{descriptionlist}
+ \item[Execution stack] Contains the predicates the interpreter is trying to prove.
+ \item[Backtracking stack] Contains the choice points (clauses) the interpreter can try.
+ \end{descriptionlist}
+
+ \item[SLD resolution] \marginnote{SLD}
+ Prolog uses SLD resolution with the following choices:
+ \begin{descriptionlist}
+ \item[Left-most] Always proves the left-most literal first.
+ \item[Depth-first] Applies the predicates following the order of definition.
+ \end{descriptionlist}
+
+ Note that the depth-first approach can be efficiently implemented (tail recursion)
+ but the termination of a Prolog program on a provable goal is not guaranteed as it may loop depending on the ordering of the clauses.
+
+ \item[Disjunction operator]
+ The operator \texttt{;} can be seen as a disjunction and makes the Prolog interpreter
+ explore the remaining SLD tree looking for alternative solutions.
+\end{description}
+
+
+
+\section{Arithmetic operators}
+\marginnote{Arithmetic operators}
+
+In Prolog:
+\begin{itemize}
+ \item Integers and floating points are built-in atoms.
+ \item Math operators are built-in function symbols.
+\end{itemize}
+Therefore, mathematical expressions are terms.
+
+\begin{description}
+ \item[\texttt{is} predicate]
+ The predicate \texttt{is} is used to evaluate and unify expressions:
+ \[ \texttt{T is Expr} \]
+ where \texttt{T} is a numerical atom or a variable and \texttt{Expr} is an expression without free variables.
+ After evaluation, the result of \texttt{Expr} is unified with \texttt{T}.
+
+ \begin{example} \phantom{}
+ \begin{lstlisting}[language={}]
+ :- X is 2+3.
+ yes X=5
+ \end{lstlisting}
+ \end{example}
+
+ Note: a term representing an expression is evaluated only with the predicate \texttt{is} (otherwise it remains as is).
+
+ \item[Relational operators]
+ Relational operators (\texttt{>}, \texttt{<}, \texttt{>=}, \texttt{=<}, \texttt{==}, \texttt{=/=}) are built-in.
+\end{description}
+
+
+
+\section{Lists}
+\marginnote{Lists}
+
+A list is defined recursively as:
+\begin{descriptionlist}
+ \item[Empty list] \texttt{[]}
+ \item[List constructor] \texttt{.(T, L)} where \texttt{T} is a term and \texttt{L} is a list.
+\end{descriptionlist}
+Note that a list always ends with an empty list.
+
+As the formal definition is impractical, some syntactic sugar has been defined:
+\begin{descriptionlist}
+ \item[List definition] \texttt{[t1, \dots, tn]} can be used to define a list.
+ \item[Head and tail] \texttt{[H | T]} where \texttt{H} is the head (term) and \texttt{T} the tail (list) can be useful for recursive calls.
+\end{descriptionlist}
+
+
+
+\section{Cut}
+\marginnote{Cut}
+
+The cut operator (\texttt{!}) allows to control the exploration of the SLD tree.
+
+A cut in a clause:
+\[ \texttt{p :- q1, \dots, qi, !, qj, \dots, qn.} \]
+makes the interpreter consider only the first choice points for \texttt{q1, \dots, qi}, dropping all the other possibilities.
+Therefore, if \texttt{qj, \dots, qn} fails, there won't be backtracking and \texttt{p} fails.
+
+\begin{example} \phantom{}\\[0.5em]
+ \begin{minipage}{0.5\textwidth}
+ \begin{lstlisting}
+ p(X) :- q(X), r(X).
+ q(1).
+ q(2).
+ r(2).
+
+ :- p(X).
+ yes X=2
+ \end{lstlisting}
+ \end{minipage}
+ \begin{minipage}{0.5\textwidth}
+ \begin{lstlisting}
+ p(X) :- q(X), !, r(X).
+ q(1).
+ q(2).
+ r(2).
+
+ :- p(X).
+ no
+ \end{lstlisting}
+ \end{minipage}
+
+ In the second case, the cut drops the choice point \texttt{q(2)} and only considers \texttt{q(1)}.
+\end{example}
+
+\begin{description}
+ \item[Mutual exclusion]
+ A cut can be useful to achieve mutual exclusion.
+ In other words, to represent a conditional branching:
+ \[ \texttt{if a(X) then b else c} \]
+ a cut can be used as follows:
+ \begin{lstlisting}
+ p(X) :- a(X), !, b.
+ p(X) :- c.
+ \end{lstlisting}
+
+ If \texttt{a(X)} succeeds, other choice points for \texttt{p} will be dropped and only \texttt{b} will be evaluated.
+ If \texttt{a(X)} fails, the second clause will be considered, therefore evaluating \texttt{c}.
+\end{description}
+
+
+
+\section{Negation}
+
+\begin{description}
+ \item[Closed-world assumption] \marginnote{Closed-world assumption}
+ Only what is stated in a program $P$ is true, everything else is false:
+ \[ \texttt{CWA}(P) = P \cup \{ \lnot A \mid A \text{ is a ground atomic formula and } P \cancel{\models} A \} \]
+
+ \begin{description}
+ \item[Non-monotonic inference rule]
+ Adding new axioms to the program may change the set of valid theorems.
+ \end{description}
+
+ As first-order logic in undecidable, closed-world assumption cannot be directly applied in practice.
+
+ \item[Negation as failure] \marginnote{Negation as failure}
+ A negated atom $\lnot A$ is considered true iff $A$ fails in finite time:
+ \[ \texttt{NF}(P) = P \cup \{ \lnot A \mid A \in \texttt{FF}(P) \} \]
+ where $\texttt{FF}(P) = \{ B \mid P \cancel{\models} B \text{ in finite time} \}$
+ is the set of atoms for which the proof fails in finite time.
+ Note that not all atoms $B$ such that $P \cancel{\models} B$ are in $\texttt{FF}(P)$.
+
+ \item[SLDNF] \marginnote{SLDNF}
+ SLD resolution with NF to solve negative atoms.
+
+ Given a goal of literals \texttt{:- L$_1$, \dots, L$_m$}, SLDNF does the following:
+ \begin{enumerate}
+ \item Select a positive or ground negative literal \texttt{L$_i$}:
+ \begin{itemize}
+ \item If \texttt{L$_i$} is positive, apply the normal SLD resolution.
+ \item If \texttt{L$_i$} = $\lnot A$, prove that $A$ fails in finite time.
+ If it succeeds, \texttt{L$_i$} fails.
+ \end{itemize}
+ \item Solve the goal \texttt{:- L$_1$, \dots, L$_{i-1}$, L$_{i+1}$, \dots L$_m$}.
+ \end{enumerate}
+
+ \begin{theorem}
+ If only positive or ground negative literal are selected during resolution, SLDNF is correct and complete.
+ \end{theorem}
+
+ \begin{description}
+ \item[Prolog SLDNF]
+ Prolog uses an incorrect implementation of SLDNF where the selection rule always chooses the left-most literal.
+ This potentially causes incorrect deductions.
+
+ \begin{proof}
+ When proving \texttt{:- \char`\\+capital(X).}, the intended meaning is:
+ \[ \exists \texttt{X}: \lnot \texttt{capital(X)} \]
+
+ In SLDNF, to prove \texttt{:- \char`\\+capital(X).}, the algorithm proves \texttt{:- capital(X).}, which results in:
+ \[ \exists \texttt{X}: \texttt{capital(X)} \]
+ and then negates the result, which corresponds to:
+ \[ \lnot (\exists \texttt{X}: \texttt{capital(X)}) \iff \forall \texttt{X}: (\lnot \texttt{capital(X)}) \]
+
+ \end{proof}
+
+ \begin{example}[Correct SLDNF resolution]
+ Given the program:
+ \begin{lstlisting}[language={}, mathescape=true]
+ capital(rome).
+ region_capital(bologna).
+ city(X) :- capital(X).
+ city(X) :- region_capital(X).
+
+ :- city(X), \+capital(X).
+ \end{lstlisting}
+ its resolution succeeds with \texttt{X=bologna} as \texttt{\char`\\+capital(X)} is ground by the unification of \texttt{city(X)}.
+ \begin{center}
+ \includegraphics[width=0.75\textwidth]{img/_sldnf_correct_example.pdf}
+ \end{center}
+ \end{example}
+
+ \begin{example}[Incorrect SLDNF resolution]
+ Given the program: \\
+ \begin{minipage}{0.45\textwidth}
+ \begin{lstlisting}[language={}, mathescape=true]
+ capital(rome).
+ region_capital(bologna).
+ city(X) :- capital(X).
+ city(X) :- region_capital(X).
+
+ :- \+capital(X), city(X).
+ \end{lstlisting}
+ \end{minipage}
+ \begin{minipage}{0.5\textwidth}
+ \includegraphics[width=0.7\linewidth]{img/_sldnf_incorrect_example.pdf}
+ \end{minipage}
+
+ its resolution fails as \texttt{\char`\\+capital(X)} is a free variable and
+ the proof of \texttt{capital(X)} is ground with \texttt{X=rome} and succeeds, therefore failing \texttt{\char`\\+capital(X)}.
+ Note that \texttt{bologna} is not tried as it does not appear in the axioms of \texttt{capital}.
+ \end{example}
+ \end{description}
+\end{description}
\ No newline at end of file