From ddaca6d9870782f8a10dc992c7fd7bec56d632ba Mon Sep 17 00:00:00 2001 From: Robert Jeutter Date: Fri, 11 Jun 2021 10:43:09 +0200 Subject: [PATCH] Vorlesung 11 --- ...Logik-variableninterpretation-beispiel.png | Bin 0 -> 35719 bytes Logik und Logikprogrammierung.md | 104 +++++++++++++++++- 2 files changed, 100 insertions(+), 4 deletions(-) create mode 100644 Assets/Logik-variableninterpretation-beispiel.png diff --git a/Assets/Logik-variableninterpretation-beispiel.png b/Assets/Logik-variableninterpretation-beispiel.png new file mode 100644 index 0000000000000000000000000000000000000000..121dc858289bcaf4d8cd028b948b13381353c368 GIT binary patch literal 35719 zcma&OWmHz-5;lw&h#&}vNGmBVAss3p4N5oC-AIRuND4|LEiEA3-5_1k-Q8W^Je+gZ z`@a9aXDyeC&))mK=bpLdnrmk3`&L@y{ylmb`IJ$`bdTrmgf2lwz@X@`WCiEmUde=Yxt3n zo*;<{y^?o~S)Xul{pN7hvNI(1Rwt)eRbIhgvC{;r&>pw<)i;dS6B{|%xJe<82la6Z ze5wZjN}1v$F=Q7zJ7o0wz0<*=Ydg8HRu`h6SW;h7H>`{g5+NlkYZlpxKAmT+X0MpA z5D~imxW4{Ac*E!VBic;ki-U#u>^v2p{qH~f1an^h2#fR=h4l5$8oi(W|M*&CL-oa> zni)GGd-S)h>a(s@tHzf9UbmCGF;;T(!NZ3_Wi|`+fp1*D{r4G|tiLT&BqFFNC>m#t z8i)S(_2=ZinerLIO+S2?WU;Bq;4}LwO*(eATj1(ef=-j)BN6gyQL&ioJ)mq1=iRKB zz(~iY?t1sXFVmE~Q%rwbS1;PA^xqxsJke!cs5+XIn5p+-fEE1s-wOIIA#_TNVAXh!%d){4#FpCvC>Yg> z&CG^#KQZezzs=JT&ev~m)^L~*9{Qu<>*rT)e{p`Ymwiv6G7|R1w7Zs5V{>`#^wQhI z&&TJOuwtSskeCO_aXqgkU8TU_=TO!8Zo6K4`2CMnE=SJv{5!Y@=&ukuVb*(a?Yn=~1*!pCCcd`IIAu?~~Q)@<;7oz&2&EUBD( zDBr(-ul;lr1*t{FhAab4VTY`lbn|z;FRURxR80LF!Hd2s3s^C1@#fn!Y2uO=%4!if z)QD268RQE44P?9HG}x^GOK>UdPd5E+qFoLlzbhw_!;~Ax!Rp|isM)NVoitp4Fr=@q zFH&fR@>hknH7)~zuA0WZ9KN^X-=8`VBe>x z<}MteSpPzM#K}rp{71F!hNk9b7RyOqq&ESNUj-6z@nXjxKLRsoK8ey>bSs%2?bf2< zxEK5yX>722*s|0;;({}`W#_CdQN1~ChN;WvpRZ)z)+>%*)cO1Pw3=TW&jqPh zyW)S;Z3#?q>KrXHHJ&Jcfdsq%rI4ve;xFUsKT0D^zh7}7qbcJWF->NF}@MzJ9W@Dp1=-XEmhQ(xP3K_+By68X3Fa@nsZ!?gDCSY?Q_F`zOA5<_pUt z192v=g39(yA=Z9$IBiuO4cB-G;L<71!|t?K2Qq|&g?Gj*Yp}4fUpM*Tt_& ze?Y?-6EjoFUy`HkF^jdR@B4R~4*`lgdh(rDN1qNIYFU?pcxdZSJIbX!Ndg zT%HdVY>#LwJKX!d^w-XHZ{sTImCl*u)HR&`1Eid#>J_tHj^f=q#3L!aE0PnK`gO75 zpvZ%Y)4lS@1gok|!)iusSPiW?+?Gt7$8`P7IO;eR=Lj&w#|IZ|TUuArHr4;s>2))s zG#4hG>XVDL;PvhHLH56Ce>CwL5B6#`a(gZbbwhq>czj1(R2mC#6tYpYm8L2i6fl*0 zv40R`Ixllo-i9(=Iq{>gsJdn4xX)lId)}B{O4WGRRv2L{Ge9FryHWSAc)`xW8B?ln zC^tX7FJ+Attd!CC)OryZ#Dn`;+({jkRim5Aqj_=Oa(veeac<1s@HCtviPff{L%ElC zN`$Cx3aHz-y7poi_H(+wzq)NyN*p*gBTa}-Ypz&o?97tEgtFm1eu{y(*g6ie)D9`t z4%xH#WG4)DXLkXVr9X@>xFXSs-M_{f617eIka&Jc>ZrqW?$~7gW_-Z=X^xA`9WkmO z-61TT-PcwoNwbBu?^^Fl5>4TWZ6$25C99k4N@G2?e;mH~Wm-OnhUAu9`>Rg1j*cj* zsCS1_U#PEMH$5?A*St0|PX;!%&gWjSkdY>1may6zdUV?6?>hpes+NGajEjL7l4X?&lUm|>(;x+?2mUZ2`Gv?y4t0Kma9!z!no`FF) zvK@2ZhEYcTxCf;QzIztgbz)nB+mS!7V0V9WUN-XDiAexo8I?mSQClpNB#G$0tGHl4 zIs7uW{E4)yHbW>ql#q7ulX~5D-KXfS6_4%H7O73Ur@j&f8GPY?uK5CUgZr64mds?m z{TZX;h{ud2V_&OcjB2r;d>-F#6}z?vh?TwaZj2Ke^Qbl7vwG(t*nRQ#DV_Y^n_+t| zFSC?z%KLLykP8`*1pmIQ&f4_7!5Q)4HW#Y(*d90_a$RJy(WG>o^r#5-?VD|d`C+>9 zR$7~dxQDJEXIT+pP-~xZqg0nd&(jzi+ z#q59o)V%)pEx zqyKbMbarsw`rP=cJyzQnQw}0M+3nB+Df$F6Fwj%M@V(JUKzIHJh8r?VpGaz=NHOgL zZTjwa;{plvU=3a@XuTwiBCX2pXQt^Re(Fp57IFQ>rs%9R_3Q4c=cN=6+vCbyyu-bu zmfnjK_)Dt?cf1OWK9{`SldnYOPu@=fO4AmFBkqy!#6mjmi=TgnSfbu&Sl2@xcE6W@ zb4HleV{5|U<=E@(PMZFPQA>`iC~$~8Kvo8BO)ZFJ4C#&M1i8FOPoKK8Z#^roEd?S#e{)yaEKKO=Azl!H&?ZBb0Hwd zL`m|L$|%30D+xC~1#wHtGL(M2X!))+qYS%$m}!aXkM5$fGf^SsN1h{YdZpB_h^2J( z=YbIWz0rG-INy)&gHKD-YTF88D^X&ef1f_T;OTyuGQQYktANTTrgxS z31fSTy~6>q6=NsR)Zt;YP-#Vvzew`;yebVx`yH=*r=hblrP-nYT+=wkw`fDj7)elk z&%le^T?p15B0lV=d#V%idgQ$*>hcL*qgK~=6`#AOh)peFQ|C8SLSY)cT~_epb1e%s z#%7eFh7qAZzZeAgJg>UP6B?Nyf~@-xr;9XMj`@4>OI%G|3OWXh3>Q*?bZs}@v?EnW z%~-xQ^@)^wDqz5SN4`?xZ)Qhxl4Kl|&-%_k{^t&|{A!xx#oM~dD#{LbXwAKFMfz(t zw<#T0M3#&3%Exbu1Sht#58L!LzF+4}R74@kN zMH5X)vC?uDdJjzVCFPK*OH!Z~K%3oYp@}*EyoPzYguH)(v#2gL>UXP-d_-FcIg1YS zg(Y)HxH=mx->HbQg=}_SDvE#i*^hUx)vw{dvfAv)D6-mj&#;D-eO;7Kdin!Vv^Y?8i ztdPR?#!oNtF<6+oe5REJdxA!lK=J~2OejJ;2W&u@`%wDo+!vH1_fPd?qDl&t0(0gjK??OT4~2v+>c z%|J#!8)6o5h~Aqg7}-p7?+L+osX>@4Q_vfOh|{WyaIr5%!dUZYzh6e~w>-@wdgbX1 zKzXQ%m|rbT2l9$av)Fw%v~y}93l4Y|UPpoP-oVd9{W2@CU{Nvd>njh98mb0c8+QKt zeyzt95X%%&6BQ0iP}Wt?*sf4od)>qRB^}G{da@7^cUQ_4QS^nN-!+l>>LF2e^l^@; zWQ^vg@8Bg<>hEU0xbD2=#7AfXGfz+#o~0V8V| zXK5Y*N}w>c+vX>W3T=_!m#0BFU2Rp>)PphV4{mxYc!AhpEo^2+pHp+`{8Ot!0edJ} z3`abSHsv<8jRb<|?F(-sO|y?t+;F~JJl+wK;*>{Q^-6Zr$de?=k1Z!a=~;SZ(&5{s`yeAZ^+uW&5)2OnQwYZ0SaYRJ@) z%kE=t^k}P2YyQ=oNJ)Y9#eU!E9_Np~*H>s6(rmpcWusBUUI3dYBS3k6t}U7`c%)@n z%|943J~4Jr?=lwQmQsnYy*TaHALCFYyNg}x|UPsxbv&x^+VD$ za2~zR&xFjahw7tR<95iCqiAxZUud0jJlv%!=UNi=wXJcLFVe}Q+L!JBhW7n##%;aV z&|dE$Q`h1#;VM&Y##Y)FI9cT)m#N4=B@-8O@}KP?4q7fvI!ieZ`6HC@ni9(v5sfd5 z`@YOJ`I}0lB-45F^a@k3PImW&#p7J*#JLR}$dFW_A2`&x2q&2Twr?`LM48z9?DB`o zT;`G0`CL{MW?j3->yoplErVNwym6RcBR(HiBto8RBSBJ83Dc)_y`%p(G!fkR{PJuI zorHJzkE#S(0q2X^fC>h&O zM0q-!GfHKz9e82bB9m`!ckakFIAUr#ODr~iN&Sb~+Mu<#*E+P$1#|rPR+(U37dB5qt@(D`@Y?LGn9^k&7D!Af6>g^#!^qJZJx;aa&H!0l(Q zrqCL;(ac0pU^O8gc{N*TFo)hinyNfIp||zp`{u^U-cpN2Nq>cdrOCgn3@$FHU?o{p zY2sZNV^vPZjK)iuA*NVZDRywc@5hb6g(`QN2|FU0Jw4)-B|nVCjz9NX{X-iwlWG!^ zM64^D$f5GwnWQ~}X(=g)zkGq5|7@K#RWhpHG^grKj%L+34niy;RjqVnM&h#3+igwA z{K;lq55OZPEnR)lg#DHc2TDGXK%zv^A7rlEbtoJZ;^e_peSA(&vrh2hPDajEN(b`I zDbhVqgQqHj{!jUR10hNwj&!jrRsz;+aS|D7YXhP7kY2gRjTuyq;~UYP%~>i1Mq|a< z{oU!RMYL|G`%mfVI~rRXhXCcQaiTl#d|!NGTY16h<$3Q_3E8$2eyzroHrnSCl$iwq z6-Ntvrg<~_e%y=G1KsoE9q{naf5Ygec8#f}V@ks-%_l3PdV1cL2r+;XxTd44o1sy` zj*5yZtu%{tdbHK;i$ndG%O=^k*EdIwC&h=*ZflbGV}W6J>d67Aq6cQ}SCYNspbhIM z$E!*m#|*|5hcPzuvm>O;DfNm=^Co`lYpz6xbVcFQ|#> za%mW>1|8E25n9rFKS5XOO@Bu|J3Cu?H0jb`xfpOkueLsw*L{iUF^0K|hjP;C{$+|2 zjpE(M_0R&`WVR#O&n~4?iUIk>-sz9!87GE8ZX|Wv$0Bvze)Uu9YBAc(q*M~N?A-1K?rd@vvB*D7Fjj^^cI;HX<6%{X5y<`HE2e`ORARn&$%T`N`BPAi} z3TIGz%F&{($N#2)gZaT zw-2$#a)&Jo72K}xKOp&^pWt)ZP)LN+&xFYEw+-x>4y4!Z%(Z~0J*1WQ0jw$|$cKRM zeqIsQ_ZHH`x_!lOYh(nSAN@ftf^Y~@@TKzTXZI)H!cq$fl(JP{fE?I#wpG*p`8FEM zK_K$&d%1QivYp^wqA#tL=u%!Wgy~$Ddt}0XJ->wg)ficrA1jo?pPZlMkF|@wz##IM zK0Vx!0JER$w2-o1#C7wZ1+;}wn@U5c0Qqx;D$RY9jEA0qj~`gSKH8iB4spw{JFaSh zh)7)kZxiHT&5*`VbLpO-3-8W&lTIFvMrbnr=;*Y@@;IbU6@6G!d@U$w{4Wc? zx3`yD2JU+v9EIYVwp52gs<*$~%YDpK3sD#>HrEo=-9v`sS)wq5ZoAag`Su0Idw@^% zQmd!^{?h2zKI*ZwsVFYEx7ax-O9SV~qTBHG{`u6^1u3gxSLFs7&h{SwJ=G$U+vD!+ z7*DjST>}VS_%-?C?SUN3eNa7MYa^E`X}!t?-ZR-cksW%cvk4V!+?E^aFRAIgl7c=l zm#x4lXz<&5@VA04DEXBTarCN%tt$=$wl>5(_5(3c798JqFi(-p2BnmOifZ>@NUP#P zW3~$LIQSLxN**z&>N(0Km2}mogh!2Ver#N+lxH(aA^8qn&?2Jog)jh*j$rl(29#@yV2Lp0; z8>3-hBCZQf#9{l?C_|P27upv^MuFpkTD3%S56{GldV)|w1#4!=4_yWuPU zJMg<=0z-Q46NuIm__n(H)l$62A4K5qh{cVHNB#V5{YgqJMwB~7MGv`J!Hbns?i=f) z*vhlb3Iv;FZ0Si9L@72Ksh_U%L`6fJJKmXNye@<%cqhb-d+MhCb2ZR-DvG=zhX zQq|Mh9;A(_i!vdqEw!HG^ti0dXvv1hv&Xts!32V^=s=kX>LShTp-K4R0h!|3zidKsk-&K%{PWQG=|AGI7>|S=40qVEW0KR} zVsH5e)2?^{8BtNu)Gf=gVg_Ip+9$gU(idlyVKj27J>W@@PxVdK5SoDjq!WYApTc9s z=Ghot06+1NKYMbu1v3S)FyB#1BWwN@rs|>~%2di(%*?6Y^#|L8nGkVa#>VkDbTM2> z2XK{9N`xCBAclU10fI0VAI~wgQS7Cy{tsVm$OrDsXc0e|2^|15C8wgPWk?X#ffg7( zuVd~?-eCGWPxG;2jWcCLN}m;*>=QROnyf4fkG}Po(i%HgT|*D~65za4^&7Aof}}U! zemQJS(yQb*cJv@UQ_g+T9?pQ+^|i5r@}24QO+KvsqkQ`G6C_#{Vn0V8gIS9Ad>8xu z^Ifsgx6vMPUZ8tKdr5RgezUb#e2`!{RV^9K{w*@{F^Sv$yAX1_9z+N^ibEL$H7?cD zr*)>Z)<_x^_LQ8Q!{oxV6=#f_VH5ZNm&zPH$1 z?egMCE1XGdbKqBKz;O8oIz+e9Y$RVuL_{v(<&Ba`==UP42?^b@wzlqw7noXoYmsZe zp^AuytIHz+g!SL@q}(D>0?$HpBugwN&bdF`Y%x=xs&2zyiP2DriiwW^;!i~z*df9ihls7yfmVcMsDtx5s-@GbyDBd z<}jGKJXwnWC^lOgGlB@>D1J9?W@hG4I;F1U<-TJ5_D6siFQ`GIPu)(vS>10t<#x2w zgr~JUZ7Gl@9&_u9#YDL^$OFK{G~5*vAio&M&mrAGfBX_Ek!1)DKtw9xh+?3m*8xjY zSryio5dOC|fkOH`F0Yk>n|m}xnCgKtm?Mgr&=7iWWN9+-sUkrni~?)+vfXV_KU)2L zM5lKSAv-B6M}jLNQOXttr2KCdz4PxTEuv!?FuVHSew_K(%=_ zM9kg)&=*DTrxwXgRI?==fOm)@2I@oYW45=gE|2Fh!LAwalD>*ef^c2kriOVe-Thl36R>MKLd!i5){X;f zk3ax2{2DGckEZc$25rWuC*f7Cd9tKTk;$M@U$Sp|H0^!!(ZU(X3iKM~14#vUpn+|$ zJzWPZ*$W;OR0Ukl)t|`>a<6ip4&tYG?h_~z`;~qQ=G@_difgWuV@eN*XKF{?r{8c^ z8sB&vHiHg+KG_akHq^(C-SX+36gc2L0MPj0& z+ovg1G*t)x)bzUJVxd%4Mcm(DwlOD5t0ssz1$s%Q%6R4jkWtT5YXNyP6O2?g%nYGw}0`&y*_xU&w{ z?ziQ3#tJjC%oQM1K<^cr$}Mn)M*p&+Xu3Pn0oy?(NC5;UaRVL7ky^_vh3z4OYUuK^ zQIY)VQ!p+^ho&C#Pp=B%0>io5yk)(`jwpJq>Tz8l!q*A@v1?IS-!>5cU~&(-TXKH?%U0lUm;MkAsWhqOGTpc*}f_{+u+mQ1CPc8%kK z1oYbqe<9Fh9ExJ6)r>U9^PLvpy#dDEodLi@9*~eoLvoGc{y+;~D4_s>I4_W?M3!Jc zb|t=WSjhEfUaQ`}ER|F$t7*=jaF<*608I^Vd`d0|YKoVoWeH$=$^{1B2DN>BflA0&FOlK&(8tgP zjBq*>CVc(!<+=O0qd`Yx9gMF?dAJ*Z8t@$|q5dotRs<*>XZ)8UsuF)SCg8B>$kS~J zZ9Ty%lJo24bUl8KP+kU=wDfB~-mq|LVeRH^5X9uu8+jw7W!TXi%jXgf+$`$y9FVL3 zj|LBv2Z)GY>F%b#zB#FfX$l)cFPZ-v=KoaiD+G1qOR<>a0Lc75I4m_wh)Xk6IBn%K z6~7tAIei5`DPK4NQ9>K)dvNp^h?epN;;1}G1*0XF-Q+>MukGv#5qo!y$syg2jf0G| z4U*R$RHP8l*Z02V0Oe5nJwpr!B}B~34`j#zN%+FES=zv`)fxaiupii#{nn(EogEu& zuY{Wd)Xrc51oa2W1xgb^HQI}h01a#S{*tNEv8%FdlK6=45upTK`i1#Q>lc|%=4^;JduQOm} zVU1C(69v}OZvU;FcBFuG&4bpo+pZ|yFyS!O2~==Uc4ZEnVaVnP3NM41@dg~YLfH;6 zG6UIq6&J1rVd#suH=-bH6ggglBz?ITfAt+mnR&*(wMp8;oPi=!CCE!1V84k|lFs_F zAZi21t{6n3P#&-JCZWJ6i_KaE3qtHeaIT%Fmy_3wjmvcCPZ2k|HH>cUa07ZHlp@Jk z?y&FQACy!}6j*I8Y>sd?z-_sl_n$#3uwQeDNkkC-DFjZ{a8L8_N&RG-fto^m-Zcic zpNW8INHNZOML7mDyh(tVY!>6g*#*`}FhIixEKeU&PUXenn1x#eD?+4jbSy5&%Y7+mbc$J4YZWo?3JjzGk>1G4 zVuN=W0v%TLrXV9zx-CwZ0%DnD7$+%^56Am53@kSkW_Ua0t_zST0S|tO2*wo1UKSql ztgytU?@tANKplb^d^%AN~W0z_Clx(Kz_^IFfa;# z^z}pQq1K!T=Onl2Qd)GF+=*=3!TfhK1tX8#=HP#{Q^if*pC zx?Bqbe*oG>!Ok8o?Eh#7N``JcccoGgS?!w^_7ai0(kX3a*h?0@rpneN{@?W8`9B5qtF3%{f zb?{}FSZ;{mTEIBa?|PNm{=rfZ5Zm0ZJ5j}^9KxRAwc*}Na&CMw{QBu zczKV;Z56$Bd~wM}hBqa0z4{zy5ipk_NDypwg<5yo@ zx?~FekOZkoo52(zB@F2u47n> zO;s$l(grm)lOc@%%|_^~bsS`7z-9-aPzZgDBnrqolpMgloeqBCcp_Yum%K*}A`@i&}dE$=^685Rwahc=)UiAzoa8<6B#_fO?vEJaIkE`bmc zD#Ty)f*}AS;pSM7x509Jlf?@$`z!r07n&eb^b9l|K#*QU{pLR)?vw<6o^LtD4+QA}pfsXxp35$o+&w14X~@-X zK*avhghPDG6hn!j!VARACL+SbLa3PS*Oh~+#}ov=qF>((tuTzmd{lNt4X|}gxvcdT z#44V$%C}7AJTd^fBw#%JN2J+^*aR5}VWEO<{`L&Hv@8rUp+>`WxSFYQ`?D&oo6n8{k+ z(t=1~FtI0yNMXMf3J@tQCk;v@rQG+g06bnoF#){JLNJWe+8^Wz<>J;`@?LwCK;q^> z&pTX(ROYtdD-z12g`gHcA|s8&(7WIe9zgwt0Q0s4*Z?#|6BPg2rKj{cfbILg5%YvY z=2FgYZ3Ks$(it?1(MHq`O-(230Z|C&Wifz!hX_!U6iIK`C6tfMVZaHYX&X+DKugyj zgM+0&{#f+?KCC{TMT=Ln(*aKNh*7=Owwo^v!I0RD=oYeHn2(0?xf~ivq+kLP9mlt>$6nO{zzl=%8~^EW~fZ~?dCuw+mzT=zOT5GoNugHQgY_&4C4M2aQiQUqTF zV!6LHHI@GuOrW8tG>0@=Y%T%bwhT$E!eOhJ9z*Gx-yUv! ziN2Jh(_j4J<&|f%APy^1gB>yMd=;j;(^-Fll4&@Hl&{wY5ygf>CHa25)H=LL`woJ4 zfuj|u7Mo>+i!(uwGiH&&U-G2_r$^r}VYHm|<}f&PgtSxT;!u5gYAT^?9R`O-(PIqH zVgthqT%F6c+;?OKb-$m0-AokZ8fXW^4JH~r>guLfFZ~WxkShOwXfjM0*CV{s6O-S_ znBD*(ncVsbuCw|tyB)~Byl?v#gjfec_4bHiJg6|quf$?Fo77dn+My{~-M?!j$$5 zOqmyOKa?BDQVB^C34%fo7mg|id~nCqB*jh|F(rF(GzC;D1w^dWWOY4RfX&PXZHTR( zUVCzrEQBZzh=?S?{0MCkNRFbnu3x`RE^Yt?k^1h6{j zcOV8c^glcchEbZ}ryAvUGeDjWeh<$7uD^Z9@^|wM^vBOX0^#26;@SEh6JrK90;~VK zZ)-!Khliz=rYLU9W;vgrOd!0JYA^nYw@ z04e7`8Aazel)3;@{oozPY(=s^li+|MFQ8?_%38D;sl-5WJp`q_u5RB=Ox^_B8RRb< zv4n=hMW%Qle!4;mK$H-S{GEUOG)J#cBiW2uV!5ljDz>T{sN>Ohtt2OFkAi|9pxT+F zum!2oRs{ufiVf9yqClO*4QUM#`>R%edg;~Q?-qk_4;mq4#4Z3-BS^xhc%w}9O~l{r zu!Ch@+VD~kd(QWNcO_Ym;KQ?{GP^i@me~DgsjT_vxo#uQd`C#<>UZ9ja9lI4r<_c; z@V+LzejtzZc~9_=_I<&nBQBO$JjOBmP&-qNWbZHG6Br}`6#fH;zOq{^O!XD=kZiu5 z82CDz!|ba`~?HUyVIi|AtFGIZgNJ13eF-d?l~ximX6sA=%y=Q;UASzS=;E z5#{vi+j&|_>)=#Ct6bxLDqyyY3R86~zpc&=Hb_n@iLWa*D^SPFTtE;ZQvnJYuP1GL6cU_zT66x_d+w9RQ)C)EuCzVf?}*p#}mJw zfqW>GDQM$Q!+O+{H-s^{rT+ERmQpS^5fctNg86)GrpH+_Z(^e=kBYC5fL7HD$oWe= zMtv^ZUlRRyJ*wlo7n`r?W7L+F7^jPdef_2o=tkJ>7-{X09^s3UF^n>`2} zdl%Ne6FS)IbL$~kMCOlr84R{SF2V!k9%2KL7@B#{9X8c71hFd`wUj zKQaMHpHe(@8j9ay?$D2E_To2){3QcP_{4!^4JIZVgL~U;j;o-?AO&XY0ufw*(lE{~ z?*cpK@h!Z6DK27DaY3@>@)pjRr&#CbE_$A43I@B=EsiN`_WZ}k)R_%Cvi2f_hmHcd z@g>}kv1$MV5D(2poG`6*J?LVNXB#C|Ha}3)?@=4?Ilf@rvE<}>92^)jd1GW~cthT} z)bEYVWK#>N;=ZV(B1>0@OX3cnBwFF#JPY|V()le^6$uq$U!N&jm3#`2MSnq(SM;7O zv03bB^SC?NP3@kM)&f=NQb%Nqm9DCZ(Dj9pgTS+&sU6}%HQUX!ug7i4AP zm>P8dnFbY8|5rZgl1qVn_kJvn+e>`Acz?Tg@n!n<4p5x3+Efj?rc6JGYSQ9Mi_|s2 zfDPHK!+`h-K2y~`HX(;aA$I^A*8jt z@xEqxpZpH`NKIase|cKDv`B(w(^UyzEN zjgR}j&~OjW0b+*Kb+Hq(INyiuO8t=Jo?a0=AwDfTG;R=(%v7vES#Trth7r^t0VI4s zLAA`e^aQ0O7)H~u&)R z@+Bb!UAz6wkIHsBty<4`4jZ!Jj@?YaybBnmi* z$KVhUh=V_?$A9BtZvD|3rR*hPJl&(Ee0uQekq4G|9+HZkPEU+Fx0%XQ3DjqtJ>ZhA zvj2Ar2w7ZG5G2 z)n4T)Q~4QE@fX9eszTy*BVk5ZpDK(}Kudab^*J)sodSmREWrN)m6#B+s9_9vlae)(MP^xFt<6I-F&xBmRs?uaf@VVF{m~WB1GYnx0{7ZOs6DDw%4T|MCou-?ny}mO-=fd|iV?)l|h23aT zc4J}~(B|C;^OX=mnDc+S4sR*DUL(2*@baX=^h*ZAU5X;P(~PcI9^3U{W{^>`F(?J0 zgCqlrwZTlIzI11^#^@(pRH9mMtOdthAx3AEo>$WuxT4I|N|ZfI^XtA=D{7fZ4|Y)f z@t9JfdJvzcKLmw*b=nf`neU!pb>Vew#w?d=ILGL|H2Kj&_wdWx%VAr_X~PDK$dEIN zk5?M%QQ7tD0izMZnIO`G9eN2es8-%&9krK=JVp(TY z&=Pqmt=;G01VJy4hZ9sSu`vI@iO&xDC<4+IW*X)3|1@ii-zetc#Tj7WJ$|cc5a9ZG z^QMQ++#)$J>Wm%}2OC!5`*@85yfi6UOq~4bSVzTLw{n6;V2(P zA7g2$=^+ns$ij$41Zbr|`x?9TjO6rPF-3Wo^CB$_d$u$ErK!HkvcX1@2QsHH(W7#s zqsTLN`}`>_k4LMk47r?6^F0_}qcYy|O3Dg+-DnEb{irRRfe>aE6Mgg>F>^#-J*wCmq?Z-w+lX2qiKl3yQ%BkCO>AG`h6ZDX~Qg-z#SJ{^WrR9MO zHFisZu2m_KDBd}yOhLPwgcK;sgc+iDAYOTjET=TpX!%4z&qO3x5Vg8tsLs^{14G^m zr(3zu2n(?S5LGyo<`^$-rQPBASMCy3V;`TYGdCEpspY#JK>|cA=ld>iS?E37j^;@Q zsn*z`AdGt@`d*b9Ph1ob2+3`dvabosm_BsjK-EH0m~~ZFSC5flM92Y+wwjJJw@n7p zf7riZJfWC8ZF!%8vd3aNk0XSB?)y#cvIy?~HsP(kPU_^i4uQux%a+G(!ELNEm3#+9 zKjEz8?9j<5I9(1#i-qN+#>ZP#k}%L$;8Mr(z);V z2yI=M+69orq~JviXVhWd&FDvb!r254PMowHe@BRHGW(tc|36?%aUWC>n5tEdrsb>U zskzNiG6=(L(C7mB1&&Xodmm~>K6`z9q@eNxj% zlV^4jC`mgX=N&W2AM9{*Pmfg~R1TPxgWv^~W69I?12ow=@uWrW`B1|+T2GCKhcsx_ z7a_hP*=Wyj48G;mS$f1K${;aubGh#$UpZw^Xy5lwcIgb?Xu;>(2`a3KG&5WZYB|vv zwU}I~2|4k@Agv0*QT``r7zi_STRqffO%*4G}`i=rN0)54%EnR4^wgHXfcxo=y{@Dms{H(v&Q)(xKF4-vo7WzB76# zEtvD8KHcoytsP>2YA;!yfgpn#b*tTD;YSxkKYHAXW=@eGpUo&Xy5foqRrAoOkl_iQ z$tRpA-L@#@m|4eF{KF$O)EX=QEF%8L1?{`v@&rq$s_wU;L4tj0DUWn8JLwcEl zJ8I&yu0BklQG=KAjKBT1mq&pyJ%?43Yc}}wkrevE$27}^|$j4kAiF7>ji^*-M2_@ro`AOgGDS{jrmP%Muvq% z6CW=T;SyxeUUccNoEVItPYqR0Q0*>s{VhyiwFqFuK};4UDT+`13Ku`>*TEtEZu7%8 zhsp}L=H#pwp5_xaHnt7hIoHMx>leodIjs8^Y*u)&<9`$0)$A&toJWaIBfUAyY^;pr z1R}eZ+A7otbZ15FC%ZXfCMGX04?)#K8=cBtnEu;79J7QO6e3#1ETa#c(uhio3c&(F zQrI(O0^O(okyLtJE|Wd0`5_6ImsTtyB=Wf_DLEPI)snvNneE=Y9Gec+^B_Vp94teC zT+2RKv@G^g6SNFqpy0-jA3ylZeEUGac8rGMv^a3uuK^d$t8ZfzcR%rV1pa;#6y#23 zzgAOH^YrC;?ivMGKFZE^!%1xURo?E&$j+WvND?-d61`?+BuF997-+FuAAaZUUIASy zCdDjeW=KpMdxDAZ;yVYtqmVE)t=tt~X7=HkG@7Y;C`nF4>QO>G=R=3dRjbPSBZ1iI zyxlGsOjr1e_vErs|8RrPR7aj{_Fj?fX)5H@eCxS4Me^moaBl=uAVH>Q2yA=-H!ndb z+8HN~%wHu%m#mCPcQl7Yo_)}Q60Fa4ysSTBB%eIaTYS;}6u)fGU~aNv^Zn7KE!7(; zvMxmUB8F2zep2+Fi2%bVrl&uP*SfBWDpk6#Tt2%uxF4**Tw6fi;K_#)55NhBQiuI?koLO~LK$2iX`&0l|$P9y^~gP!z*&0_Sxe+0$`bnY*_}hA-WC39Gr@Yz4Wex?HUdwtT80nQ1feGCnt< z*D~jn>`(JI;GP`b3Vhe(6~&Fk9KW@)CtKn3!_P& zklic+bm8@h3MH`^$DBF0>Aw~xUfGH6*%hwU1Ss1p=~sE{Yo7EmkN@%=E!wSBbj7h? z7v7r1&}y~%{Aed0g+`I$i;l3(TQ-Hy;o+fTYT|GD6f;L-ImXXUmbIdu+hW%IvFspz zihrfK@bkdixW^u6iaw_uCkVG|+sz`Wp_;OG<)h`*1Dxw#2OFUw3#GN@EU2U~6Tl2Z zxOGcQ)3wa4@Irz$kbh99DcqDoN>i@*Y727A7sg4uPwZZFZLg}0<&JH1JXUL1F?@_V zD&UR%N1+GS__faz%O;*VSm zS9Gh}(c<)$C*Cu68I0fZtui@7?Qbu9*$k$!LsSZ9k!-^+8-i+L$Tp|^AGSt^xoma4 zn&_!m{KIcP#eX{`l~5wq>HR{mDa9#U>ei?D_;VIl zs@+k1+KKIz3W-Z0k^?TP*ipHq15uJ(4)OZwg=G2AJUZ&)&<7d0^J?|Yy9#14x99<% z)1Y(wTQOT4s1?K~yjfe|Q}dsa2PH*(ww7;@ll+w}J!)C)C-M@R9#sxH@m?1jSYKs% zTW{Mv)rykhA7&0j_ck#mV+y%+FK26Fx7(b-3T%hL6SaIHYJ^r_dx@_S_e}(mk0&$@n zo~KGvdQzZ(&KgSL(~B{Ai)=0O1cl4~?kPvZWmzwcl26t{C(K(Tr-ZSQ?IW+%q?q#z zOAiAXLc>5d#Ufma`C%A=vmj6M6s zKlq*aQcADUaHUg0fIRyRuJsD4DiZ1VuX1TK0~!7`{89I~%A|I&nU}g)$l1S=-qDbX zzoLJBh02Zcu}0wd>{I+ylSi>pFU5fhEqFZ)WZ3R6zY|`2Fe^LZD)``)4{A&(2g-D3Hoe^!nZCd?>(F@ii{#A5PzhcZDTKj+_Ns zVdtt?Se?+E#{{Ly@c0EXnR<>)7MXInw|KzCl{<+s<-|>dl`qaYT8t z=i)W+*ZCvw*Xka54d>cCjqxVh-Wa#2+<5~jp0e@9jg>}X?pvn+>Q;*$s5yydi{BPu|vEp6|||GFS;u|<2V1mn$7~M zs^@$AbV^7!BHc)L3J6GdE8X3VTsl-z;DR6^NK1EjH%fPRx9{-%{a@E|>4Gbsb7s!W zp1q&vvt6Q#pDLI}V6yUa+>NqQNfUROJGOV8IIK;ivurIt%vRIU*semF`}_J{@$e)~ zO=&1)3hO@Z7nXH~W6d@M^aTyP>@8H3d`N$D+$zgu2vRcoiAs{pNQP{oTf8i?F1g665D5H-{Ye z-a8*MW&^e}Jim$hHz4qT#MOiyR^cxq9TW6CdM_>x6C50jfPnC<1cZZwV+-(REvcm| zjnd0mOGbV&St@2ebzX5@-}CY4!S8zTk0U*fHJ=SG*1N9Puqs;L88=YMoPp&ia3npa zI4}v+lGKTgQELbzb*Ph&G{AL=#U><&uQU!mlx2&P(L&@W)sf_lX555nDfm5H{~iV} zNsHiw+V2Lw>EfOAH`@+X1zmLdG&LWehV~B@3|a2L_{k3lmTkROQZw8R*CtnF=u5NIv-qA4MflxIBd}WD zZH@a%sWy`CDD7Pq--^V344Ge_oN)fsjD4jf!)Q1Ns$YP0^%dI_73yl5fJ_-yHY4u* z>xa3HKXrn_ct@p4m0Nc&hewRGGL;aR8)>k^e+0R~C0cM)_68vl3DcLB7P_vxU@4cU zI~XjKy76kq$!dkxs7lShv2*gRoULlUY^Tz)=kHb?EX~gOZu|Kq+rLvHb;@Pfwyc(x zp})W^g{4+%E|ylW&&!JKYRkM%QLp6Tbllze$Gq^ zn@m5B#98A5(~|&HXGt9yk32V#qoX6B9#h~OksQHYtLf?}nS5nKqKSB7Z zhMu#xAQz8_h*RT z#-`VO4cWtg(rSKQfyM8F=y#k$MsvMwl&$BiEatiC28USQAa;j&Uuj|~BPVA(u)HZm zRDN0aT*JZ5UcSU9^ZD}X10@6JH}C5v+2F{6j5mXqFo{>P)(q-vTY^g4PgHW- z6>`x%t!M_tAXc@ti38iO@jfrARSnNmSd{BF%WltKsr+F))3W`pgs%d^LV=WG z?9E}A0mJ->U%ExOYHn#FUEH zW*25Kkeg8Bsy{sO7O6; z7$T8k>SkZvlhsVOH3<3_Lq!<0p6Rpj2MHo)m-_x%M#E3om~t|Vh;2Ym^%ul>5PmKJ3;Lrdj(7Zd zZuoJnU*$}NtI7}D>$Z>f*bH1;I6($Oy@4}f8pF!H(K^`3>c(Ekr@=l-kiF=?&vz}wO3zeQeClQWGh6xB+ z{6R$_%Z(AU`&4ov{`2bY?4b!)LZQ2pk06slB)qiWPUn<*v<4cs%e0lp}-w>0SaO@(R{gS0zBr4yc`~C-V4T^rAU$ZjOoKaiS%b<_fkY zO~NK|*_oNd$^ z`x=J_h$bnMpmS_!O+(t*0>7_@k=n=s;=R{-PG_~lXQHX(;nx0ld5R$VQhG1LD6Ocf zs`?Bl0P1WbFzv$DA$8~5?XB#IOr$G67(dVmJV3B&*K({_YsxXmrTXbM$9s3qR_|kt z0)d=4Wc483vE_}I|6-7q>w+p=niZ2~HY*Sy1Bv37jEv!km()a}S&1LvrwGcdUAG(z zk`{eAy*{=F@Y;#$`_G@YI_A25IR{ELD1?8t%PdiCYIAp24&>uwG}8K+^` z`=MN@RvmLSpguzW$0qFAthvWtqGdb&5}rrEm#_5aXsgJ8df6c@b0ehpXus#)@dA0} z=C{Gxl_gH?F7pKkL3Kz1Ha!%a%+REIK2whJ%o=op7`qHi z*LHBJN$@Kl3NoYR3<4|QxkDziJf;)rMq9JxsnS6xjLA|%Q5~+bdFb3 zQjurM>r(GQ8i*CO0Ln_FUNYJ&RDCXis%iH~DoleMQf*qXTFAIMUnM(LdZ1S9+GTh6 z%~frJ!P0d2Q?ozn{^8&eyl&TFqqw9Cn|crO$(E$UY(Q-A>Y}bgi4Y#<&nnLP|DEZHihCRuH=BW+H4cwBf=lt@_S*08}MYdR#dPO3rNUl8Z*ivPa_L|G?@5|A zH8lZwJ@AqJ3|v08BU>*&F5p?&oayRC+ev*#Ks{C-S7Y_2g~9@}q&`#9B7T_5tl|qV zU2_Mo+e3;$#aLy(JQZ7xV4~p*tFpl>u@8I#kmoFK8;2jH(-t3LNxLs?Mzh4AC@%g`Uq z{VsP_P7vM1&8-aQG}-xZX1d0hE2dkVFOU=Kb_ip_+&MompxWgiE_`Se*;7oyifRQ@ z=}Zm78f>*2lMKUM4VT8K0sV-iM=)74Q)2gs8fIWRX-hOm!4va8gCfigQ(phLGTd$OAe3ik!3IXpFHx0Gl|f7mGr@T}=q?|)QpxKh_2WaDdVI_Q}c^3}Bw;<^42zlqKc`WG*&k>PH}v_kLq zO~;gPFb(z)fi_pIhm;PXiqM%ptHPDQ>Z7>r`{}sEUR#e<7(Jg3YR?YR^Yn{Lh!sm! zXn6Sg*4E4oZfa4aBw1b0TwT8LT=&&ts-2;K$=}b-9ustuA$~e%SK`bXTe&n~6QIdS z{PBiU&6?yM%XzshDExc)K?j}h0R6js7#*#mL9+%e=tpwa`UaP`F6!o9`txmcuYQ(G zgHUmm%^;6iu)Uo>eU=6qZIWG5O83IKbSxGfO}{(5?7Gs5#bq*?YeC@Aapd6phtL6N zB3Nt8%(Ue{MghbF7dVJy`W^}7Dg3s*5}S?p82E9XPJ*LM?3wyExQOuu&-bsRd>iL4 z^XNn@u$hiJ)lY+FzS-} zb#bkEZ_&l^=HTB8leqkiap{q7xE-{Q0A2)~LUM3WD;02R1LTNoNS(|dy}eR1e1uqn-SHW(e@&U<`(v|=4j@5aYTw;ap)o)e7H>W?M= zYeQgzE_EaB7>On2iv#YsNU1xlN*^ni_sg{llhcS33*ncGKi<#9ug4$T8Lr`QLxI^#5h)mYX@QYGe>Lw^)JIzIJ7}vY2wutywRL zg8a;fh6BMKhurhf1MCaXLl;lv{b2>uKA$V?f$=_vF3yDIk%b|SQ}ib>$qKyNgVefj zrx$!+HZ>mK+}~A7-yGZ3!U9dFy+jNqoU1Mst0FYJk&2%szhWqTo$VKdg$zhj^ogh9 z$Ofr*bq=#E`tlt^U*a4{S*f^6cFf|m{)2<>7+S{LTggVpBS@MoOEI_IgJ8!g%7AAE zq{+RBjOyUniwuuEP}&pr$2hHkxp`L>`+mLW8t;@6ouUzgyua;T6G~g`uc{Bsf=2Wy z?idG3x1^g7G9JzI+bc>8dXi4++$$Kg>BLsHl#CyScDZKQ-!T+2RRP{JkR}tL+FR(| z{>64^2_&tg*eiXhjW;jb#HfkO*2-Ii_;=?_qN>Gbupi0GwXE3Me4qD}T zU4!OD=eY_aKe!4#P}#NH3#)-bp?kmkdI5-7GCkF9Ja%xHjqdhass!tw@UfLGH=9=l zJR6tWzPO@q()OtZIbZ+C>HmE1+v{!Qy^S3hz;60SvhFo;9$qr2iGva~Em-Iv{@-!6 zRbZADi_fNh??k*x*U{s|n+zxzq6=AOq#bFKSmyDU!aN`UszbbG@ncg2cO;jK?Bs>* zK#=8xUL6w&&rky)L6gJjKI$fbvgZhvPh;3)R{uOy)BUJukn~fBG$q~8H&*ZLw{XkN z_=(`Eo&;-wKn5Hux=pP2?Xdqtjc9C1Yupd-qMp{Wjt88uMS|gz_Cv4p%@(a+{nq^g z&K+`nu*)54OG``tJJQ44A9d-f@*6e9#5q-XBa*Z8jeS+fhNK$2igO9z$kul!WUY%P z@DnFEXQb)s65E=wB8DVOBxRo^kzDJ}wKu-to8vvXvv6O9blNaf$>k3VzCY~QG&d&m z7j`LL&AJ-uO!<8PU`a@P^xS>nO2IYDg@H@1&5`pda-UaibuVm;9mtovcdCnK^3J*x z8c`4Ts9}{*2x)T?*VLX#GT@k|5W&@EF66BFgK-7bh!<1j1;+@0N zF2sd(SN#l4mBrl|uS6x!DL=5IRo6gl${h$wc}u*kszn-VW%K{F0LKlCR&_5FGcb)B zb`ANzC_zI2``ogmv%0dP0#M89_TA@5OuLoH+VN3X;moS*3v1^DZPz5$Jl2ioAg3J66XL7hrI#l(}0t&2Q2g1vto#+*iV zgm{Hh<9%B!;i+`!z>kzWtkf=bdErfHaZ?E&(_M}QUgm<_xx&2>Uc734h$YL)VqDmm zAnfP|WMxUHVf>gyHrO(~1-fapk8X5$?rv_eE<@&6O&`E(_>0WnPRXkL5vjU|OlipC zucz$a>VI&j_mzFa%z3FPX;01ildZMv*GgzVYQHWr{9AI)EDI3sNj}_#@@odAr>BXF zvENqz7i6_b~dkBc!B*I=rp|nnJba4yOjTZ z1amHQ2D;8xwIIR8){7BXg_pDKUQx&gdkeK#kVU60@<0j9HbwcHI~K-<6o=1I9m3~* zW(M5iHvV9b`@5#^#K)T}m zFh~*h3jE!ca3B+ zq>|>xHYPVq*$ZdmFP)VWhGSZ3asjVU+mmR|mi!v(s6aBcQ zsZS!w`#GCOtSvPQoWp<&<}1Kq%rqVYsbBTddwO630bCV5SauecVxv0Oo}gJ3tMoUf zNI=emGxz>WLW1duR7jdc3817*2Yx=PTgQ9`4uX+uZ*SLH&ZzjQ`5oiq!{hw7OBK(Q z{hscw%#Z#Tx-eT}^F`w@$Q=dRdS|g;CG#tL|us?_A2T*&I4M-ZE;F`Ou0@FtV?G{4`Gue6Q{#wJ}%Q zv+Nxunl)#+xb$S-V$`C3KC3@K@y|TBBEHjYjaRL$cjKj$z^+W`I9$kSf%9PAq1tXt z@!!x!ynuj!o7>x$6h{9rQmH*oawjb)OeI(a1X3sSmEnOM?|Sde0_c*E0fYqK2&N7q ziageN9g223Fm~4Gt%BgKCP$+GHHt(KPqJ}&{VU-^c)lVb4@;sZW0Y(bffaq7PLMTu zuCzkxF+^geLgICO*zI#VO?&1J7zO#BrWcvM;4+USKdh-w{!<%mv3 z(>9@Sgcjz*IGz*Ukh#{d2eRsGt@?}22=-7?*Dn<@j&cg z8uvR4qk7Hz1HEU zy~)OoK`Cjz+IU_9VXqRw$#K8mB&8)y8?4=O25Q?%OQ{eEJ4D16xPPCGOB3cO^jr=L z{6|gaN^9%ufMllLK-T@&eXqZNcr#@n=!#_t366|~Cc1dQ7^{Rwp3$aouOqK+%%`m| z2=t&(J#GPRxM{R!U=olh@l3;(0iRp7WQI%*6*YCp#)cUX31PJXcPYpyIn|G8aTQEI z0>?fcs7GmWcywpYU~3=r7%rA!fJ-g6ShtR&+a6=>I?>I%zq0%>U0DA^mN{oMDP42u z-k4_nsMO>LS6ipZj0zH3D8oqq{#%w4Z3i(1r6?32tWcf*ct;El3>3yVo$%heb;e>Z zz>3HvmM0o4<>%hrWqUEH{ zT=ea$k2`HOUVM`-chI=NHLe?nX;fYZkk)p zOA>45BxYuwWxnTb210R=2&AJ<0(Y@bM)WRFqbu8zdJ_^KnH(iTKNwUaPQOBg4OjL1 z*irUP>7P(8Z36>?OBou?^{;>&xDLdKWuisHi;Ig^$m{^W2U0~odj3s1$I^7CR8g~Mjx!#<6~o}6EJS!3i{{E8>hY<1=c=~kl97fp6@Lp{uoQz z8Y%u%GMDjKy*?Ozai+Q@GNk6jTYUiRv(J64J&~G3_Dq zr>m?L@3LarCq8n@H#l7qqua;E%JR;%7ZF2naB)HL?X`eFy-{0HBjzYra@pC-mPRsh zrVc`i+}D4;e_^7s%-eLU3g>*!=ET4l9(O3bOR&)yRHWxR+VzU<*uiTuuj#;~XQ4VY zPh*0vIBsi0?z5tT}#J1Yubz)C9A&H526o3>O%3R3`UN-WvGxVP2 zl@W<2%O&jH4$X4zs??m{LE2p6v@|s30K1?EJ35BM{1c(6L84?!TThR~rn*7PDKX1} za?fL(b7Wtq?t%jZ4&K5QjUCgvvMNrl$xR|-#l5-TC*SN{5y>lD9>g@nDFy#Lc4CB- zvw~f!2Ai0;AMoDfi}jI`f-l};%;I%unXAixN!!TU16i4Y`P`2xusa|AWa(dgk)xP*q4=-(gMn-a zOKG!6*w@*r?IP(A)y6^MEXhAy;33Ua0j?KF3RzzSX#b^ZqRYp0Zv86jvU!vw#0bAa zDX-gy2-C1W!VmT2?oDlUiX)jjJ3q&W6QQG}{hFMNByMG8A$m*L6~G?!z5m!+6z4BQ+NKuSu zF^x>A)8ypj$OPRYz?%6Rfc^GtL3sbci98cQc;9Az3B4LE1Qv587sAgl>nfT<6m;{b zE5m+%@#P4Lef1Vhb{P2ynGJ3bTh*RDipePEfF6#@)0hhKhy;qVG^2`uus%zfjf!U8YyB zf`Woz65y8rK~ir&tpT=dZ?qPuI(Y9e4<d2*_S1HcPPo*PyE_PO2>VHTpC$05p+B6XCpI=qwvlIV49tS=E)GHvqHf+3vulOB_ zdy7sk)we}tk5Zu(!Bz2F4)`&_usw4~s~sE%#z0|zFIFS~Kprkji_mOlV}i*V%_$HSI=d76kLOH5UODkViku^> zbwcg1y1IEfJ=&^i44eM`eir?j;w5*G#x3Pbrk5D5hYEXFEG>u9VR?BFfSw^<$1s)4 z!hMCKVP9?>*&44baBA5TR@g+J^9jW%>^b50<4t+{{(CzvAXV#IVZqvU{OM2YE76yw zXscyx8AR0&`fM8;@932nEI#}*THq{Yul&A)K`Se#2L*ki%)0uTVe4l->nAP=j&#RZ}~UnD-67c_i!`WM6Og)^^^%VUtf`E|!yomLm&!bmSn4X9GU#`KOQKojAAfq=Q>&qc=O}7o^Mi z_@=}(9ZppEitI>irtDc|{s z=Frg5_cNsFBozNhE(TrC=!Y#MC<6-Cpil-)mFvswc2NidPrkXWIibuyP#>ZQ^yb6u zML1b%YN@ieyh%9h9>ht#Ju`ZJ{K8^45P7an{v#K76DPJ>VOJ4w$=v_E5O zqIpV=&}YpCx8$zcYR*Lge{Lp>qVN2aB|OgB!2++_3)*zY(=DYmKA%UbsJa9ehn`sP zs#4ED!93v+#Fm`mC4asw3)anQ2VY{(u+@I2CY9{MYP!<$@^T|SGoUp?+V=sZn0@j9 zR&XnNnr%gQL90MM&g*jsq+B>88>W>(*Q0Ug2L9)CEk2&0>)%rK_&zRfW&QqXU|oQY ztWn@8Q_&0^-fJo)2J2f-j>}&?WkqsD!QHMaU&Bk(6R=_Kg!!*^9!K;;G*$@U?2Rh* zbZh9SMn*2TS#riXmt&~mYgF1eTq5#lrA`Z5`~~WVXue+{QRwqkCFRgZ#_yHog9cwi zfPkjw=%)B7t=yKUhfz6iGa)fv_N=v@CU4_(OEx@Kv{{biJ&PzXjD;)ad759s0+5>v3*3LDw(kV1AJcBc>6)`2vtIL zVtF*CnR<_*8MbErpjHZ!7wITc$lQxqdMV)Es>5mjlY;Qx}8{m2}v3}1r zt*4n%x& zqk`?wB@JA$B6i?aTY0>6ot@tRrr8QGLejIde+Ge|zE+VFYeUJGM=A^Cy0kfe7?NJG zj=m=;gGTIkquLE<(r=xTg-$m<;_@;5VhmB6j7QY2jdYbbz7jdLRk< zCxALQ!=L3z6ha=4O`quU>$tg!gh7tSYZhQ_3p>-5^5I_r*F6vb=sfv!xNrEOHRy~H z>Rx#z303)_2#0gq8={r})2)pwG34#)&fad-;r%&{#M<8WhKte@%IoHE5F-#67;S^o zL41qswNAM*T%L{JYRplqeCf{vzw}RpbW{Nyi^LC;U76?n`@Z@3eyz>A+`BJ)ph894 zg-Qi5wtIQ4$4smt&AzLJQI`$i9BcvjWY1j=5)%^@%2ex0*WM1olLfWZtr5YYI`fWo zQ({6j8qm@evQWr5+B&e2vBO9(Ho2vwnS3}Ey@p)P##^&n3A$BUK8oClG_sZ|p!jC9 z-H;B9&TmvNWzILw99LFE%Z;+EE#uxk{N5yc^qpOf=+gj23!K(tINTohmMP9q>{5r> zqo`l$YiiNoUk@5~H@a?Bpo2r}(dI^f*m7@%u=m7{QitT!RJ%R%_0mf>Yh^X)7)>?9 zFc?@T>~h1^*LGz@{+q32N!_EXVNn`cV=?us$BgT~@Iu-%fc8Q#Yc>?ixAbRYlo6o~ zczqJt+G!m0sy9DR7cjC`9`}1uK|&aq8WL+M#Jlf5Yv*XC`}xbuqm7DOL%Yl9kEs$Z zi~h|9)Ht=}iAA=oio7NZeGKOh6g#>6gf5uJ{QFlClaP}y;|9}<@A%W-_y=w=DIMCw zT`v4&*_KuNNT^AnZU{#0(cvU|A+v4JMr_PpB}{NkyZd_cn0j$+`B!qk?ve1DXLF1I zI#rsuju=Bl6FTyWVXYa1`&3sgaeeVMLQ9%VJY!6P&|+26}Rp*3n+S`Hwqc+eV ze5ayYUK0LOgxfQ-)i&Qr3Xau|<^Z>%aLd1U%jbNAAx_fN{)F(-dQksE&0UpXqSemX3o zpfrw!ozL|D)Fg$wyVM7kcXVS2v3P3)B58%IPEG??T71)=>O)ncG7gk<)gMaTELtkU ziw{hYuB;Vx%4Q&jn+gMwerwnNNs#8(ICX@}u&|UH-|xDF@>mN==?e%cFxU<2d6^OH zL}5_EEzOW#_}o~*zRxtfzk}>E4F(-3XPZ%Gl?0;H4WM5LTJaL-@h{(N_o6y0i((uH zVwuM|)r4e0NC;1w z%AI{c5oH74t zCNz2a)HR7cK@o-#_VoB+!hWowdO{OTJ8vE-Pd1zXrTiq53~RLnzAS2;AuNSRQt22I z8GYB`AJmW@W<%+m2?nZ9FP=)A)3Ls2uU}U>o3`-uke5j3ebNta|Gdm-7>TXOeE%3l z`J|LpTo(gGdFMy@vJ8xGo=hLdeH+eJ(-oa`3d==52dpsXSWBW%?YYMAIK#jrw~3e@ zKH+ZoCz*>Yd+ zzuhrVvQB*kO!$+jknD#_ADZo}nC*k3(}!von$L@~7@nT^Ibj|ub$TB;6@BxVvBAvC zC(Fl0cDi7IywGfjLNZsAx8)}CG4+C&u+ifNm09&HYQ#$I-liFdiuX!fR3Vg#55Guz zL*W=QYR<)kKlBYQdP%bsiK;m7gUChzx(|BoL=Cd}rh#X##Z!!kY*Dg9@xwCq>o6ir zoBYYM)BPPp5+2ok_1lvov$ZRutb#fy1=XzemN~1v?bbV$w7UdszBL z@^5t1t2_L9KRMz`C+b+tx8s>1ZXd{ptua}061&Y9)twZSy>?&j{83GvCG42vE|D-U zbi*eYtXJuJxWW6M;y)EiTj{pl#h z`H}PfTGjN-q_u9iUdrG&AQ{U*1H#Xn7`ApJ-?aIxdclkktQqzhrRT|jv_U5&Ox-9bBgo( zU==HN#mL>OL*JIqxwi|etk0`BZR52qP-hK2G*U;&^STKB!5>amB<$a^mh)o;=2#)1 zbeS(>t5K8Q*;W0tZ;>kH!EX(x{g&iFE@TP;;lf`7=12zI~|I{@h2BVVL?w z)LK$$$LscB(YFaBzo#CeKu2qecARR_qzxqw)o(B`XuEQ6B{UKZp8h7aE88lM7v_<+ z2Do4tHWG`zGx!rRKrY;wSPE7Q2)Sz$k2BBZEQG02gtA|Y}?WJz8}fS{j}?Uc*DFjy=zS&v57rS*I4e3LVqA(Ugf zzBPI25a{tFnhCA_j9)a#z&v@r@h=o7pc<<9li&Z1*9#E0u6`I89Mr9KAjcBDc?FWK zoy*IV#>U2=i;m87Ib;)+D(#zT2Cn7M{J+rc<=`_HX`=vv`u8OVl_HU(u2yokRf##4 z$e}E+Qj#>LX5jI|tscr3Q~EY|q9Wf8s?F(D2V|K*D%2JJRO0IiJ=N?>exqHdWf1t` zhHo*Mk~rzQ;e!+JdU~RAewLuk;p_%OF60%TsoIq(MX2-G%h;mt9#3d_v683TY$NjY zr?noBFeM>XeP~uJuY6-akT|fJa+!tX{khhaZ({VM>pqOfBSjfp%Eh~ zHQ`ONQyez($s`BX}!)WnHYw=>&?EzCrf--Ikh*4StkO6Y_-zB7+4{@LBnl#*i&~s%4(V;$&Syma3sQIVkXtH0m6}I-3 zomXwAfa8Jr)7o1gb?7f$meq#hGTJHRAs)-Q^wn|M56C2&-{A8ppTs1ch1B{ zE_cCypNc766G%-E9hcJgQOIW@xU`^-1cPt2n<&khaCavd`NYBue*G&bsLCdu2@HRW z!kEdcv;J_#aI>Yb--)Y(@+EMj8Ibt^oS-S47Qm(2Vge69its_ll*ZrKPTM_Be|YptzXJ zns9=iyHr_E{`}h@Ohsk{0!J`7^t`+Te0+RAmA{YV$|V5Ss!ZAJIiM0hQ;SYP_op+^ z8iK=mf~IJ8!+;8Nr46?3(1Ab0oKHwQO=fg4w=#`0AP2G2z8dqWnwZ0~#@+}V!ICRq zxTQ0XY`bWhZ(21zyagtyQGzSWxhV&E?G2Nu6?dL0XtoUh4`%xXXw;2F&tipK+t%4eJz_auG7rcyY#0E+!JImu-!c* zt3G^U`de4z)NYF(RWwIHt&VeWHWvommu*}CG@dp7te>wuc zQ;(8?qJn5x3ZbL~>INaRVXVY$;+teQm!M^9DPMguTBmJyj(dTfzms=mv=Hk4M+&qV ztpm)R+y+bo#r!xUzY8BRA4Bgq1)JuCTvtb|c8jU)eN=~kZYJL$7P(01i<~q&CSn$7IOk5aY$pM(BHp*y?oMYq-wC?IJvk`F)``r>BEsJ zyn;ZnS7SH6P{1=HB#NBb*cj$qwD6|6!*XDnC-nS5oOn@nRjONtA*`h(A77*nGV((n zQOdW?mc6q)g08>-#Zm)ln*!ppo(|z}Fl^+iJO3T{PQE{X+kAL;z7pR@n%`WlvAzXe@xZU<0FuL;2%Js^`v(Ao*+p((*fQf+4epuERXfoXnnS z)YU(tw;Q;xsi|Q>Rp&Jg&D+%|HkXCY7R5X*?U)xbPsY;U^e@Q0tnmLnbbaAUlEtE# za7t#g+6c&5sK%ZmSn@)pQz}0YfH)D8oV4Jd1;F@!o#@t)Zf&uD7ePE2UlxCRc+LG3 zA)+AhQ6O7lsfnW*8B6IfD!(>;!n}bXiQa3O1y?N{*>gZjdE77 z{Gl2Wj^sdrgzFeQ@1WW6nu<)J2VKR3WPse-m1gye21S-NvOOV_VWbmBeSQ6N{}fOu z%=Fn~1Y})fM-3Oyh~fpAj=cT`(Rfj9>07aI5HnF3~%C)~mX|*Ytup2nMBlIZd`=* z#zU+)nLMqyD64|ywO^CH2XZyOMK@fPmpgubetU*ofWrM>3RX-gKRA1?0-f273E_zjBru`4D>u8N5R80ScvFfT+E1%#{rdg z&^PY6u(`3lJ-=A$Bgr2HzU*^-qzDw+6ciNC4Jn@sD*(hCpP4xVdOJS5I67)a_ z>1=?Rw@6VEiY>`avyDFXi0X6y=YDM4X^KJ!lKcsPy5R&su4iD`C20mLvFJ0B7pR4LE!;us zQ8J>(j1}@j1ZSfwPu;q`guW_3VpkplYEle*d?}#M)(L1f^V@QiLRdru^j{@n59Ay7J%mez}c*Y1RN+MvjfM7 zQHe>0zOiv?e4!_TmUbmiNDaa6hy;Q*NfZVACwOn>tb-;ypVw?^))I>(em{d|vGa;v zN}{Ynp0A-RkLd;;yw1%^9Z+UF1+Fr1Lk~58CFAy z%~s25La*4+t%M}DcObw+2d)(ewqgm*OOUN!^uqTOd9H&ZYa-IU0q z?`>r{z*G3Qxx!dAGU#Q4;Chyp3WWG}ipJm-8sN+p#vO1;EPXeXXANs(JXZBdVo!;cLty8rvks`!5+^89HCJYY@y-={G* b{=sTiU7vc7&U}CYzvQHq-j+&!`1Jn(up}&y literal 0 HcmV?d00001 diff --git a/Logik und Logikprogrammierung.md b/Logik und Logikprogrammierung.md index 7da142f..8bd6be1 100644 --- a/Logik und Logikprogrammierung.md +++ b/Logik und Logikprogrammierung.md @@ -1964,7 +1964,7 @@ Beweis: $\Gamma$ konsistent heißt $\Gamma\not\vdash\bot$. Obiger Beweis gibt ei ## Vollständigkeit und Korrektheit für die Prädikatenlogik > Satz > -> Seien $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sum$-Formel. Dann gilt $\Gamma\vfash\varphi\Leftrightarrow \Gamma\Vdash\varphi$. +> Seien $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sum$-Formel. Dann gilt $\Gamma\vdash\varphi\Leftrightarrow \Gamma\Vdash\varphi$. > Insbesondere ist eine $\sum$-Formel genau dann allgemeingültig, wenn sie ein Theorem ist. Beweis: Folgt unmittelbar aus Korrektheitssatz und Vollständigkeitssatz. @@ -2005,7 +2005,7 @@ Beweis: für $n\in\mathbb{N}$ setze $\varphi_n=\exists x_1 \exists x_2 ...\exist - $\Rightarrow$ A hat $\geq n$ Elemente (für alle $n\in\mathbb{N}$) ### Folgerung 2: Löwenheim-Skolem -> Frage: Gibt es eine Menge $\Gamma$ von $\sum$-Formeln, so dass für alle Strukturen $A$ gilt: $A\Vdash\Gamma \Leftrightarrow A\congruent (\mathbb{R},+,*, 0 , 1 )$? +> Frage: Gibt es eine Menge $\Gamma$ von $\sum$-Formeln, so dass für alle Strukturen $A$ gilt: $A\Vdash\Gamma \Leftrightarrow A\cong (\mathbb{R},+,*, 0 , 1 )$? > Satz von Löwenheim-Skolem > @@ -2020,7 +2020,7 @@ Die Frage auf der vorherigen Folie muß also verneint werden: - angenommen, $\Gamma$ wäre eine solche Menge - $\Rightarrow |\Gamma|\leq \mathbb{N}_0$ - $\Rightarrow \Gamma$ hat ein höchstens abzählbar unendliches Modell $A$ -- $\Rightarrow A\not\congruent (\mathbb{R},+,*, 0 , 1 )$ +- $\Rightarrow A\not\cong (\mathbb{R},+,*, 0 , 1 )$ ### Folgerung 3: Semi-Entscheidbarkeit @@ -2086,7 +2086,7 @@ Beweis: per Induktion über $n\geq 0$. - und damit $(f_{u_{i_1} u_{i_2} ...u_{i_n}}^B(e^B), f_{v_{i_1} v_{i_2}...v_{i_n}}^B(e^B) \in R^B$ - wegen $B\Vdash\psi_I$. - IS: Seien $n>0$ und $1\leq i_1 ,i_2 ,...,i_n\leq k$. - - Mit $u=u_{i2} u_{i3} ...u_{in}$ und $v=v_{i2} v_{i3} ...v_{in}$ gilt nach IV $(f_u^B(e^B),f_v^B(e^B))\in R^B$. Wegen $B\Vdash\psi_I$ folgt $f_{u_{i_1} u_{i_2} ...u_{i_n}}^B(e^B), f_{v_{i_1} v_{i_2}...v_{i_n}}^B(e^B) = (f_{u_{i1}}^B (f_u^B(e^B)),f_{v_{i1}^B (f_v^B(e^B)))\in RB$. + - Mit $u=u_{i2} u_{i3} ...u_{in}$ und $v=v_{i2} v_{i3} ...v_{in}$ gilt nach IV $(f_u^B(e^B),f_v^B(e^B))\in R^B$. Wegen $B\Vdash\psi_I$ folgt $f_{u_{i_1} u_{i_2} ...u_{i_n}}^B(e^B), f_{v_{i_1} v_{i_2}...v_{i_n}}^B(e^B) = (f_{u_{i1}}^B (f_u^B(e^B)),f_{v_{i1}}^B (f_v^B(e^B)))\in RB$. > Lemma > @@ -2133,3 +2133,99 @@ einer natürlichen Zahl $c$. Bemerkung: Es gibt $\sum$-Formeln - $mod(x_1,x_2 ,y)$ mit $N\Vdash_{\alpha} mod \Leftrightarrow \alpha (x_1) mod\alpha (x_2) =\alpha (y)$. - $γ(x_1 ,x_2 ,x_3 ,y)$ mit $N\Vdash_{\alpha} γ\Leftrightarrow \alpha(x_1) mod(1+\alpha(x_2)*(\alpha (x3)+1)) =\alpha (y)$. + +> Satz +> +> Sei $A$ eine Struktur, so dass $Th(A)$ semi-entscheidbar ist. Dann ist $Th(A)$ entscheidbar. + +> Korollar +> Die Menge $TH(N)$ der Aussagen $\varphi$ mit $N\Vdash\varphi$ ist nicht semi-entscheidbar. + +> Korollar (1. Gödelscher Unvollständigkeitssatz) +> +> Sei $Gamma$ eine semi-entscheidbare Menge von Sätzen mit $N\Vdash\gamma$ für alle $\gamma\in\Gamma$. Dann existiert ein Satz $\varphi$ mit $\Gamma\not\vdash\varphi$ und $\Gamma\not\vdash\lnot\varphi$ (d.h. "$\Gamma$ ist nicht vollständig"). + +## 2. Semi Entscheidungsverfahren für allgemeingültige Formeln +bekanntes Verfahren mittels natürlichem Schließen: Suche hypothesenlose Deduktion mit Konklusion $\psi$. + +Jetzt alternatives Verfahren, das auf den Endlichkeitssatz der Aussagenlogik zurückgreift: +- Berechne aus $\sum$-Formel $\psi$ eine Menge E von aussagenlogischen Formeln mit $E$ unerfüllbar $\Leftrightarrow\lnot\psi$ unerfüllbar $\Leftrightarrow\psi$ allgemeingültig +- Suche endliche unerfüllbare Teilmenge $E'$ von $E$ + +Kern des Verfahrens ist es also, aus $\sum$-Formel $\varphi$ eine Menge $E$ aussagenlogischer Formeln zu berechnen mit $\varphi$ unerfüllbar $\Leftrightarrow$ E unerfüllbar. + +Hierzu werden wir die Formel $\varphi$ zunächst in zwei Schritten (Gleichungsfreiheit und Skolem-Form) vereinfachen, wobei die Formel erfüllbar bzw unerfüllbar bleiben muss. + +> Definition +> +> Zwei $\sum$-Formeln $\varphi$ und $\psi$ heißen erfüllbarkeitsäquivalent, wenn gilt: $\varphi$ ist erfüllbar $\Leftrightarrow\psi$ ist erfüllbar + +Unsere Vereinfachungen müssen also erfüllbarkeitsäquivalente Formeln liefern. + +### Elimination von Gleichungen +> Definition +> +> Eine $\sum$-Formel ist gleichungsfrei, wenn sie keine Teilformel der Form $s=t$ enthält. + +Ziel: aus einer $\sum$ Formel $\varphi$ soll eine erfüllbarkeitsäquivalente gleichungsfreue Formel $\varphi'$ berechnet werden + +Bemerkung: Man kann i.a. keine äquivalente gleichungsfreie Formel $\varphi'$ angeben, da es eine solche z.B. zu $\varphi=(\forall x\forall y:x=y)$ nicht gibt. + +Idee: Die Formel $\varphi'$ entsteht aus $\varphi$, indem alle Teilformeln der Form $x=y$ durch $GI(x,y)$ ersetzt werden, wobei $GI$ ein neues Relationssymbol ist. + +Notationen +- Sei $\sum=(\Omega,Rel,ar)$ endliche Signatur und $\varphi$ $\sum$-Formel +- $\sum_{GI} = (\Omega, Rel\bigcup^+\{GI\},ar_{GI})$ mit $ar_{GI}(f)$ für alle $f\in\Omega\cup Rel$ und $ar_{GI}(GI)=2$ +- Für eine $\sum$-Formel $\varphi$ bezeichnet $\varphi_{GI}$ die $\sum_{GI}$-Formel, die aus $\varphi$ entsthet, indem alle Vorkommen und Teilformen $s=t$ durch $GI(s,t)$ ersetzt werden. + +Behauptung: $\varphi$ erfüllbar $\Rightarrow \varphi_{GI}$ erfüllbar + +Behauptung: es gilt nicht $\varphi$ erfüllbar $\Leftarrow\varphi_{GI}$ erfüllbar + +> Definition +> +> Sei A eine $\sum$-Struktur und $\sim$ eine binäre Relation auf $U_A$. Die Relation $\sim$ heißt Kongruenz auf A, wenn gilt: +> - $\sim$ ist eine Äquivalentrelation (d.h. reflexiv, transitiv und symmetrisch) +> - für alle $f\in\Omega$ mit $k=ar(f)$ und alle $a_1,b_1,...,a_k,b_k\in U_A$ gilt $a_1\sim b_1,a_2\sim b_2,...,a_k\sim b_k\Rightarrow f^A(a_1,...,a_k)\sim f^A(b_1,...,b_k)$ +> - für alle $R\in Rel$ mit $k=ar(R)$ und alle $a_1,b_1,...,a_k,b_k\in U_A$ gilt $a_1\sim b_1,...,a_k\sim b_k,(a_1,...,a_k)\in R^A\Rightarrow (b_1,...,b_k)\in R^A$. + +> Definition +> +> Sei $A$ eine $\sum$-Struktur und $\sim$ eine Kongruenz auf A. +> 1. Für $a\in U_A$ sei $[a]=\{b\in U_A|a\sim b\}$ die Äquivalenzklasse von a bzgl $\sim$. +> 2. Dann definieren wir den Quotienten $B=A\backslash \sim$ von $A$ bzgl $\sim$ wie folgt: +> - $U_B=U_A\backslash\sim = \{[a]|a\in U_A\}$ +> - Für jedes $f\in\Omega$ mit $ar(f)=k$ und alle $a_1,...,a_k\in\U_A$ setzten wir $f^B([a_1],...,[a_k])=[f^A(a_1,...,a_k)]$ +> - für jede $R\in Rel$ mit $ar(R)=k$ setzten wir $R^B=\{([a_1],[a_2],...,[a_k])|(a_1,...,a_k)\in R^A\}$ +> 3. Sei $p:Var\rightarrow U_A$ Variableninterpretation. Dann definieren die Variableninterpretation $p\backslash\sim: Var\rightarrowU_B:x\rightarrow[p(x)]$. + +Veranschaulichung: ![](Assets/Logik-variableninterpretation-beispiel.png) + +> Lemma 1 +> +> Sei A Struktur, $p:Var\rightarrow U_A$ Variableninterpretation und $\sim$ Kongruenz. Seien weiter $B=A\backslash\sim$ und $p_B=p\backslash\sim$. Dann gilt für jeden Term $:[p(t)]=p_B(t)$ + +Beweis: per Induktion über den Aufbau des Terms t + +> Lemma 2 +> +> Sei $A$ $\sum$-Struktur, $\sim$ Kongruenz und $B=A\backslash\sim$. Dann gilt für alle $R\in Rel$ mit $k=ar(R)$ und alle $c_1,...,c_k\in U_A$: $([c_1],[c_2],...,[c_k])\in R^B\Leftrightarrow (c_1,c_2,...,c_k)\in R^A$ + +> Satz +> +> Seien $A$ $\sum_{GI}$-Struktur und $p:Var\rightarrow U_A$ Variableninterpretation, so dass $\sim=GI^A$ Kongruenz auf A ist. +> Seien $B=A\backslash\sim$ und $p_B=p\backslash\sim$. +> Dann gilt für alle $\sum$-Formeln $\varphi: A\Vdash_p \varphi_{GI} \Leftrightarrow B\Vdash_{p_B} \varphi$ + +Beweis: per Induktion über den Aufbau der Formel $\varphi$ + +> Lemma +> +> Aus einer endlichen Signatur $\sum$ kann ein gleichungsfreuer Horn-Satz $Kong_{\sum}$ über $\sum_{GI}$ berechnet werden, so dass für alle $\sum_{GI}$-Strukturen $A$ gilt: $A\Vdash Kong_{\sum} \Leftrightarrow GI^A$ ist eine Kongruenz + +> Satz +> +> Aus einer endlichen Signatur $\sum$ und einer $\sum$-Formel $\varphi$ kann eine gleichungsfreie und erfüllbarkeitsäquivalente $\sum_{GI}$-Formel $\varphi'$ berechnet werden. Ist $\varphi$ Horn Formel, so ist auch $\varphi'$ Horn Formel. + +Beweis: Setzte $\varphi' =\varphi_{GI}\wedge Kong_{\sum}$ und zeige: $\varphi$ erfüllbar $\Leftrightarrow \varphi'$ erfüllbar. +