From 685a05ff9c626d81403c89c9d83e5e27a0997e18 Mon Sep 17 00:00:00 2001 From: Robert Jeutter Date: Fri, 28 May 2021 14:53:03 +0200 Subject: [PATCH] Vorlesung 7 - Kapitel 2 --- Assets/Logik-prädikatenlogik-graph.png | Bin 0 -> 16312 bytes Logik und Logikprogrammierung.md | 299 ++++++++++++++++++++++--- 2 files changed, 269 insertions(+), 30 deletions(-) create mode 100644 Assets/Logik-prädikatenlogik-graph.png diff --git a/Assets/Logik-prädikatenlogik-graph.png b/Assets/Logik-prädikatenlogik-graph.png new file mode 100644 index 0000000000000000000000000000000000000000..f058da7ab309a91648f74853986025710d83dfc2 GIT binary patch literal 16312 zcmb`uc{o-7+cvyNWoFAfw#~6+mLfADNr;WgJZ8ucGH1?4#xj&-2q9CHka-FjqD+yf zBtn_T=UV;l`+45uc<Y)QM>mO48XVRANF8Fyyc^OUYRQ~yQDMQ{A&AE@ zM~ag(QbbzDhW_8YtVjCydtaD#zDk|se}6oz`&4k5i&*L6100q+M>*`+m8J3O zpI_Sv`Qwk}?<5%tFH;R27aFh#CL zoXV#c*VkPd_x@bmTkYf`rJx9dX@(uA$sTbUeC1|7Tx!PjBxtATYS6I`zZH^#(ARhV z^0Ue~lOkQ+-OANYBLmN`3d_pL@ti-;5yvVmG;*-F{g?TSD?2r(d|{)ET`zN6TU)kK zscB`$dpy_aJmKhLRIJ&KAD(sf^r-6UQh$7Loe&yIj5B{*|42{XcLnkM@xEQOaW53M zQmNF4M_e4kcE&Zlu1-$jaL-frth?27!4moAcU?NmQw?N@$hFrA¡xJ=aK!=ycy zG~(H{5J4H4n&EZPw_Bmefa2ly{3$H}*WY@P8Oss*}_ zwX3`P`qaTJG3@NI9||r%d}C~A7{0UqYj!aA!fXG{)6b2|PTOzAGR(;9TcW0l-1_xV zq<(*6;#)Yeue`Cc+REmps89dc7)z;Xbqg$BLUJy;kuUU0^#3$T#`rDkX5z0NsLzik+9n4fo;to1y8nm z>wIY{l9ZH`kdzdfkU;Ao#R`Ad7Djr;XT)WQ%c}Imm`-17n(Iz>|2f3xwK$4ljXS2S ztPJ)YYE;}FeDIemJTj8|+_{X)f9&wMly~3zGR0jdW$OCt{HH8cLbkB!8?@jCVI|D7o`Ov>?s30T$0?4bP} ze2sJZU?A+;@!;U#fQ>PGI*pD|35X`D#UnZ9jX|$(%@8{c7g~BXmXzSOc6PWG6`%YN zr6+%=%MfW)9HEgbt|f?M+x9$wjgp3`^2Wqg+y;3!F zo7yVYtAGBqeCv7GP8D6jhTaL!kdvduQReEvCk;(a(wC;CCV|OGN&odbhfgm!;yKU9 zEk~UocIS^x?(XDk_aieiGtu$!55y!oKF-`` zByXRd<~r}UrsU-%<@B+{#Io+uBlhs9sM(FBiLL(N10L(}*wW_oh%VR`3ZYbTgJ(KL zFF(I_pUu`US_wYf43<#eI0M%qwt?@3nU;3ExL)_J`VO8ybEhO`d z8{_#0tx+_p`TENF`ZK>j*D=)eynnCJmmxi~un@Dj=sY-U5v$a(`CKUU-U$IZ#P3_G zv5<4_h*NiW_dN&>ny*|xCyAfSiH;^ERx*BZ4PxQ?uTLK&`{h+npFTaDf04;=^Rv$> zUfysd0V3AYWNmVEw3W3r8B%Ier7`U5I{o$%LW*!G2GzHCgA1HQq=F9uu5{YRM!7_H zm0Yi5T(191ogsZQa&mIgWAh$qzv7{MJcnH5?Oz{fiVCt?AQTG+Of8O8sS_^wp7L;Y zJqGQ@zrVXVn`(UHE(|s)IeF&m*HH8~;Lw^nI&B{=E5^;VM$P8lR|u_=yHStN z>x#Y+xPFyb2||I8&oYFbxgS3+APx}c)YPPIFBlRlK}6#Y1j}BV@?TCQ5GZahji+*+ z_v1CarsIgmsePYn@SmHTQ$yyv5_$4}e{S%9m?7n;GV=T?PpQ#GwLB(5P7ZgsRfdFZ zjGzkkBxy%W1cmyYDaC_T8hCcYntrYSlfVrYqHIW97|h_^BgaV*Dt6ffh*j%L4^Cef zdJ`?4Z&{Imn46muD-|1+3f;cGwWJWV=esXm)UHAs0|t5JNuB2pU1BAOrd3-eW;M=O zWEeuG{-?4V4ce}*u5$|u+7C}(=jP6Vfzu)o&B^eM~aOLG~!rOD+TmpA`DfqE3@|%>5vRb`*`*Kv!35$r@Z$ed+q#! z(7}VyGce>ge*gVj7iOLdp6t<&QRsR3Qi|}^lCsqbOH^go$Bhiv`MB*@!-}0i#$UTz z7uB>d?ZGa3%@1J5-`p0?FDNi$4;xm&-kR&e5RT5mSB4FKw~3V?XYg?6fCtkdP9x75 zAPFZ#N0XD2lOnaXwJZVeqcJ?BNZ{YTGj^RVhUiQJc9&j}gqYSiYpDenEMBkk7TILG zLQ9Zw8BfU=4cPwn@F%#RU7RAUgwuy-RM+1IjD3C5&J5$mF~(+RpCncShkTZlMCSz2 zgD4wJ@uAZXm>e<>7~xwM7M}uEoyl?BK)hb?BJr@3G;;FH875fLv~#zGAU8(B*Wk%4 ziw1xY*w1;9ekwEX3_VJLE@95)Ckle6PKi4%LV}us)mBnbA(lUXUgW?eRylW2so;a< z`$uQfmG|=0V`SjjrOa4P zpM~L~JfmXU9>I4Wt6$ZtBx4H;1^4I5UcEX4+t`yGan5U=w#ZP(!^fup7I6^r-u#az z!TgGfiq8!SsEM+{BMGasVzw3)38a<`d19(=f-Wy&$Exg4Agq#hu~(J~E@f&sRhybi zmooz9k-R7d&?^71UQgXbMnVFxS?W|Jyomsan|IL>)R|DJBV4EVI* z&Fx=FQBhHOH;q!j8W>KUKK)`qg4DM4Iitd*OqsaQ&`@U$K@!x9f8B_uVw0goAXGiT z&7Q(AQV9PUF*d&fUh#A7=ZE|kPh{Og0gC8Cl*?aSTqNH;oaH(!*Lq4TC?v#<&~tEz zEO_>~zP+fW^|atgPzF5OW;(5a*Y{H#!_VQO6A&v0YCY}iS3B6y6jxbUS$_MMkzv^l zj!YSs(1#BnHopb%(+S}|F(DxYGIS4nt-E2d5moU1I@7i5*U{Jy+h)4gD{TDYBw!8> zId3&^hs3O`c)-y)kb}3thV;sAoX2q6Q(C!H>z_kc0JgvYZYzT2Mk5-yj*L)lVM&|_ z3V^~WhI(hf3tw6^6Qkyj?m&G*!_WQA=}&I8_IY8i3MW`#SQo%B!CJ0cezYW9YYgH5 zgssX!WSc`RFO=g) z1>cf9H$DC0 zMnjBgwUgzqkEQctRRY9Ej#LC61|dxsxB~M8pCTb(XBN|M1M?+fOU+*8xX*Sli&-GB zu5tERca9Ym6_L`=TnIZxB?iGr_(G{tNiDYySzAYkK7`EqrB~B0Ze{MgOBF_4diZUi zKe3XDiHXDoM>bM{nA_mW5IKb9A971dCPPTO(A?bY^`(g@J=gFwco4)h6`|C3g_2lF zNy(qvKb{nvGI-WSo4zyzftdB2SK*Z(!MN*hQqawZbe@8hi2Q-$<&~16M;EXD&fi$4 z;6HO(5TA(zE@!Dh^~f9leq-x*-Le<}$wv^PCMO1jtme8B3$NrJgVZhJ?nPmzyk~`tCL4# zdAS&DkQQyCi|4m@4A&a`7$CPu7MbtwtfRXE`*)AqngoyIRVf}($sJ6a?EmzM3DAwE zmR90Pp$WcIr@Bk}DSQLoyrw&9#yog`#F?TsEu^|f zJYEN!@+VCF%$t3{OWp155kY&a7szreucINbUtt&bxiNTpUV$rU3k&H)iy2mkP{}(t zT46muUM(E7^HX3AaQaZq(W6J1C2UAdU%AFXHU5tN>5{nDydGLP3LBLaRxSYsS_Q;1 z0|m{>%1Q$EoNcR&n#vompP_sgAAI@t(7dBJT~gSYiHYfWwP{?P&+=DrP6-VMe}F~I zV`F0uV6hQ0FS4_d<%Ug8ex0L4ocJm}nFvA94x`aj0U$!^5*7(gSDk;gxl>Z*QuwvG!y8nc3MR0s;b1;)XQV z{DBRS1c1#IxQ0;xMnb!B1;@;gt6y|$XU(xa^hKK!ix&{3!MOJn$~wzbEf?b!py=dMb;@*{BtKNS};4nkyf;yK!{I zSCNc|3&$uS;W4LKwF86=zkSRLl|Q#%NY`B;D@yQXFh-aEE2>>(P2Fr(?vmu&`C2OE23ni ztl{>6$(=a&m>Pq@A%jw;l!kZR9U=)UjRvRb3ZJwh61*rj8ly== zh-izh7HGSc!prQeo)^)sVin%q2LKZ+8|9#~yTnXO{$5+wm zv&0Lb_n=pt^U;rj|NCRne?9`)VkOKC6)Bz7O?crgsb*%`TPL5mW6?|2qERFA@{qd-EQwY&D73mX<6p4vdbVCr4k^7f1q7dyD-lp$tBDS-+d>?{OC4=}8MheU}>;)0CG1*wHXF>Zc zS$aEE+KH*D`HeU9^+Q)@JHw*OeOIl90l8nBrcu~JAf&IXu2#rWtBzK}=841RVK7rC zxNq~RWrM318kcc~4E<&N^{K40J6T{5vMGx2zU{PkbXWn-O@kV#kg;t*He`tm9PzJ3 z1udpl2z!~^h6$JeBxG+dpf^qYh_usi(@_4!p6W)Fh=C9bNFm$om1|PWQHxA4qc$)j zwKmqC`iMIe&5>#v8eco&*w6|C(8kplfof_b2V1i=5D1ZwIoSAT=twzWq!p2P(sXse zVJO^m9+QxAn_`!=e~q79~@0WTr zq$%!mo>$S)p#%VWvAQn!P@yB9gF;kP6n4`r`1vlT0jksJFdE1~jrZEf?!1l#uZ zcHxbNH_cj?kkJ|!HY6MBqn!vm1a)BD&Li`OK>%pFt!o(m{rLSy>ZU6LKfQdHsy~%T zY(VaN?tFrUyaysp!M@R9Lobt@TaD601O|C6Za{-Oq z2IzSGM7vIVVRUo}M>r3PykPt&e|5FyGZ>Y|eNHN~t@$Iw#E|Ojs`25AEvBL3PQ!u# z6Nv$qRleKWAeo>|6oa7S?O2mkQNuTLhhlc7SA`e+Cuo1&80fgcFZ;8d_pJfD3^-Mz zq?~p>0DdMZRw^h@BFRqhcd@TpmpnEh#Y?v86&cEUey21`6#CMuLh}51IBa$fq&|nK z`m@|TJnl>5((-<5q_DcJ7eyPwp=8N+n||BX)s-OWjNE@%Xl5pe{IX+)xy{|vwLaNl zg^uC*eD31sx-;wZgJHT)6t4f2gqlwSe8&qQ-6@rqY~Z+pIGoN$@!8qgpS3@-l5gwy zhr2|RmY6qk%6Tse`qY00YOFkP*L!d0SDD87A3(aaL)oy}Big8mdG^_Y>SBvgp3`V# zbjZ{0zAF2EE1-ITJd@cuD{0poQdK1hLvN=Zd{G|BXDO^N4f}4PiFQge|MGJ_h)%np{S6K&gxGUteAv^1WNx_v{aeR(Z_;v zF#BpcXtsenwaLm7%Wzc%h*BxmxbA+>+qc!Buu4ct;nfbUvk?8fVL5)bgt#CMhzMz{qOn;mzE8#&JX`v1k zzrYyt2Bg6V!x4-{VE5pVGnoTH6}Lc_!R3K5QxQ9lvC_WLs%lxuBJ zvFP|sfeK=^UOG_|I~*!*(G;Q|bwoV4l~9RO%h$&O(++j3ppU481fAmHo+OIzaZ>Ro%O_XQ_Z)0Yppa6G)Xm-k&>`oHIJ&-uqAV8x71R_z-(2(TI>b=Q| ziVC!N0s1-&eU9h%-o!bVAOEv#q`_5C%AE?)rU?1vda1$<3aSfb4I3F(Ts9ZSRH2mN zc5`#nFEX41#-#e@r)RF8-wZxF>$$e{k8Xq*8N+(>+BJ5fY^b{Rff{d?0W>=|Goy^m zKQs@*+zvREX!Vx`IS2Wxu>YkG?4Jc#7D~q@?*;;S!|+?5FG)j8LQ;|pA?Z)4A$ zV+CC1FkFZMN<#hKMO<4Aud_NOFff(&P*0r_7ayDpf&@_}RYglH*ZM!nRfFdK!0Z%3 zG^gj{5`DMjandf5sD?ZLOK*$L@2Lg?kiJ^eC%C;Mu_?qoc8vco$%^9~SS$(9(GyoA zGel)G8(#QJ;8$aFg&faQ;Qw` z>YS}smi!)#Bqo&2v~6FZ>VECGkr;Vc(B>1zFnKAMhUs$56MSem&H_L^T1RY=TQqIa|4&IWW1AB zhK!3g0?ThL1tkTsQqMzC(Gfc!cy}azfu$QROu^g95a4(EN>)qn@;wMI?V7%2XUPwh zd1WIBOSyb2Z6yKx#v0~=5&@8dji1M@9P{Sl;zDb&;RaxDT3cI>z%o*B%KKV;zl;@q zU;~NuAhNxMGF)3zNh#!N$1624k_!CmTUd}E%dOhUWzVJ_u*&bReLzBh2k7`B$$G|> zl3T^q^##kI+3|}c)?my5p^SK3uS&s(r@%v`{w7Og^*pL7yKn#w=L-zyV39$Ahf7xA zh6x}S3P(rBW0x0&1O<_mSB0Y#-^n{5+izblw5SlHs1-OP+``_>EN(?IzbX-2Vp7#% z!3MS8+Tz#=Sknu&K3S+Xm!6)!^5;*bTm{m50-)`E%L=h0W*7>kjQkly4A?lN32>bD zb#s^nkc{Hi9h8F|No<~ylf9} z_>keo;6rks7vm?M8EU;2Y8j!eD$nm#QHr6Q1$MFt=mwDR!eFLYMMbW`!NF((LHNum zr~7G1mgNk0Tk?k}!PCeP273Cmeacf36huYuTW{IK_K6{SHa2;bm@)p1!(YmF;o8yV zpC>*hI8nDIip#XZQw+SWhPStz7Pip5aon*q~z0&@`u_1-BJDTda!+wPhO z!li)r0)$$g>#$?iE{!S2r$wK)VI;;eKQl8~F478@vcT26M%+4%k9EWamp5O)qB;yKI#hk*7!(7$|5>6}CN$uiw0} z0=0M)*mjV<-NDIGatES4M)8Y8N}t%!(9p_4aT&Le5INv7W_e#RV43d@4Cu{$|8BLn zwTfDh>s0-zJI*!QW0bRX%WqpDmaYOT%>&*Jo3^$0w|}tG_Tu8iD;f~anx3jg^|D?Z z#av5oKO49sg~~gTRBY%N?Bc9tDz%dzpTJ<0KRml6S=67WmE6_W7Y90$W-9wb*G^`vi+^u`$?U)J>d}%R{)%Keg6Cy z)haFPz^4;I#BKm+&VL`}q==P(1d#M?gfIt8hzcSUr!0iW=`;8hL6x=GzK!WMl3VY zV_o~Tn!U9(ua_PCf^%QlvT&m_1k2G>X6$E3+-3$kA50Y7${Cf(~dZg5dfI_gzPpBf3J?Nk_CA|P0 zAW&wY^dQ|skzDv4D4NN;V5C?cp4L2tNdB`QhK9;*y6L2xhS7GH;+Kc{7atBZ1_z@B z0OUETv)|v{VqABmjx9>1g*O0#oS1WGm39h;TzT@;DKbzuWNI75-5sS^t9By8!!3ZT z170(->&n<^DC$}bE}xG82%Rx$oICghgdCZo`=+HD0Az+fd|3Yk;V!zRMJ3>1`$r+v za1nt7h>+mOvS-hx+la?Sw6|#LFc2muulf4(_P0XW+NKzOkFrZFX# zLjBO&n;%P>-5U2JMa*ilZ#4MXwO>1xlfinNUrH)P#&y!cYZs!xhZ>iOUe;nz1yWK| zZQjBUZx*&W( zjcjCll?Q};SUR<=tSm!3-odE;YO^P!hLw{YKz8C%qnm$ZfgLC`sp1DPW$9sVO-e>4 z?myK$d578m84M1EO;D4#cuddD*(94Y&HVaB05JF!6hC~W4H>*s928EHVKeCC;W2cm9}^R!0=kd5&+kd0 zT{7WIaUvfwBY3xC!rT`}#hu0~^Sk%K-;_ZHj~`s}SsGXW{rk7q_8;5iPKk)LG-juX zn$p1~RB{E~z2Nn0S(McUXH$mTURrlj=kAtVs~yVg-_nBeveewL8X~>WguRUoEz-^O zz5>tO3@cCwfq{Rs4*Gr0|Lv6o1%6Lx;$WqfX71Ooi{N6?0&2-WCtiuh0X6q~vev+{ zuD4fbVd7QUV&((q2nd<9h{x^Qe8|gNGc7{9IB3*C^mKLODKQE+J{$>wB|Q04)>$>S zX_CqY2H6Rv4JuW5El+*UUheDZX$937^%ylZwY00Q(#Nr-M#Upr8xw9lrN6ddAy>zbY~3QKq=bye%&e)nw-R>sYo*Lq8I`ZcVeBoJ@t2NhEipAU1(86I zRUtrD+I2FGn3&iBKxJj;ILwb&X?1lqDZbSomZGPJ0*YNFaHrlN4O3HAxG@35H7IAl zf*c2SdsibD?YUBm{V4y!ypg)ph~lws)Q>EGY9NVj`S`r@##efRc(8981rn2#;}8h~ z^($xn#`w+G0o#>9`@O(6pota&!Bg16mA`+hw0oiIYXauTeQo|ql~D$3T%P_MLh7#q zE^0sM38D%8p@y)TJ-~O8kniswn=SZRT4IT^!Mx2*Nlb)D5`<6!J(7ki9`>J*1$;Lx z8yf-8K_a(x8x)pA2%zMZ@tb8V^#yCeLiLk%?t-cYuczP^5}KOH1KqnU6Nqo+VSs^Z( zd}xams3|p?==ap{Jy8u8gT>Nt$AhzeYlSBMDp@2N_yh>0&p}fn$_Cx}>iB6v!DyE_ z7G`TXlF=aMNJ)aW=A}!i?V->F_si#{(Z>5|m;}$+vn&mM>tE?g5N(bqaq7DQOBW!s*v1USmwP)|_ux&*h?Jn|>&)}ga)VW1P$YfLM{DE* zcf9;oz7WN+NJc{IB$_;50^ZL6Ge->(F7ZwCSkRExgvYf&w?jwW__t0(AMBkxkQ^L>&`tv!}H~GAu%AoOJL8E z#brf|YG2x!%z2R=ADgLK&nUEc38+xPR2OC|NQA@C84|Y9mMH$oo3wmijPpgLVF+Jp z!q%2ACC9npxd^=NGz$h8KWI_3fc^!5G^x!B&=wR{P#`enJ4;2+#54<1dh z9RS7v{EFMZXQxf<7A2;8&Sf6B&S0z<+dS@MTU`I=oiIc_{;Hi8N(vRVmrf%>4d1$Y zd-EW>>A_|TKR&|(P`hFKdnP?QyAIH20JE`U{yffP7oDS;0Mq~MJ2Oo$F4P&>o`be= zfa-6+zj*?uITjNs&MxPzqxeG%lsRIHp?l;1T65N*_ihL}N-l9ubJ99r0G+L`l7rY; z5op*J1PUmf(op&C&viap`T8h&J$v@-6-dtA{qw-(5oH6W$zTW*v39M_#i^{%7MH!H zJ0)QYG#GMG2>acXmI$iSeLn(_BFVczq(Y~MnOlRcH)TyUbB$`qQq-LlBh4dea<%Ch z8RSisOY=};7gqM6y<3k~di(m0h6p{BnV^8=4ajsJG7X5^P9GMlUMd-2IU_{|QHY+7PVAhx zW?Wj0s>Ro~duttRZqXa^`OPq6gx^>NR}`A2s;o@Zmo6Cvx|7=Nh2f|Cmof$b|LPv6 z;Y_g&D3bO0&5m|$q1gl)<1kCL{u_%k3sDi}_!Q;B@V)g<=KSls(9O*5s(-~5u#%uQ zEbg^^+T)A_i8M2^#GX)Dp_Yvmz=tsh&NWQOOrIYjd-3DwKFAI;nJUi$L$Iv=QE2~Uu>w1ALN)$sU5U4e=PNM7! zW`>4s=@A%tM>**B<@1xlmisKjpv=Pys)e_IC4;VSBpccbG&VsOoxOL7C!y7w6lkSfD4?7b)gp_rmlHBFVxZTA z<@1e#4>Mrl^5$2_^o`}-aT_XDR#owFT)213Zk6Pju4_kUXVuXnl3M2|WP--gvci|x zpgmMXv%Sj^4c(d)#;RFODcaGx1*#SnCykZgq0Oz(67dvBo~=)f2N5ugZi&;zig{6z zghMMQzHkxEJ2GxlXj2y2V+m5?GHZUy)$BRSa&*?aUR-qWY4(H>$6-a0F2w~daA zYu}s>b{pcYUw0<~0Fw^J>6R&R|CC&iDxMGl;&Y%>J{0 zXoJ|b{RE;K>|uLK_oe1g*|Vp1XD90KNJ4K1+K9l*%iDFD-dS-@eQbI|KujI?n*7hG zw@#)E6)IUk#=M!zJQ~ymlRY4Swx+L7C&hXxe+k|V4OJl!z=b5Le22VCOslmwoK-Bq zwa`i%*o3pi31r^_C#X&ussIjo?ksG>piLhGEfcwr292sXh(q_$UTTVn*cB21o#ODe z&Q9SHbT1#>Z+@bbpV(_6H|>(C~1L~<_b8YkXh)R60sEJ z0>Mp<52Sdkh)5r{_$2Uh%yQm12>sS4U?3>bP;6YL0dius>J|C;Oar!i;>nruPRh#G&U@B(pQB%MFM8L@lLVM|6sW4~*uD)^RF|0*9; zm`9<>$}3GM+CmQ6x5~lNe0_cKa=c;atI&!ZZAV>Na#^~?EGS>~8Y-rccfwdel+@PB zBol)T{yvLPRoF#@M$=+2ccH1Ak(^Cs@Wi7ILltP37lY2GT9u?&K!3B)job`WMV!K1 zrz!Yb>-6-KrKq^44i$iIO4qn_wYABi0ABPP`JP-e3tlIad5IJqgn7_5-{~9m4oiAz z5~IPcE<{%^p^j$_f~faR3D0K5s} z+^cC)j&vv_fz2)Dh#Az$l23<&0yaxxY2#Qyu_;TwGH^Iz`~K%%mOxP%R2AB zXe2n_Xx2X#G|Ci1Pk1MUt??6dgI*TkY9di%%{FtE5t>&}Fx#*><;gsOZQ5u(xbldq$l-Fd2tEOL6jtDQsIBF) z!k40s0D9JNg%d0~kwMPL+Gn3>6KqZ=7?j+jC0dK!8D_!vk<8D-N!{jZG`gkW&V1Pqj4z0_v~gy1;N|mY44{-SBOm`4_{Fw~QCXO*SdLYJbfa|GFvGBQjTmP3ywdSD+| z$RS@qCI>CF*2a1akPD!p=MoZDK3MQCOm<72Zxf0)hr)cf)Ix zwBT)9=`5XUS7b=G{5=eWC~~AGuux1Zo`gdYuxz=^Z2C2HbWBW9aPTGiTqK=KloITb z(Ti){8?A}xqnK=kv9x2{u*rh&Q8cP|ET#f``8OHnL+B&LU``O3k(7USD0sYmGy(G1 z3^b$@uZ)I9H=mgfI0AjL>f>mrBS#nU8j=nBW_mdNVEicG1bX?Min^N3_1dK4soD{c zzgpoi3n+8n4@R|LaS-orE_Vu-)rV3roxWxCl$PF7HLD~XZ>2oyz1IiVTQ*c3@nPv8@yEUhaCeLWxmtL&^ynjg(VM;Pb>vP$j3$tl_R_NT7^(nl@9t*q zZ&R|##Qq28uN*8l9_j+&g!avAU%Di{`@>>RnZ5%0&7XqIh(TiR-xu{!Ec^gAVt7fP7*E(fR%2s;K!}9V%9-Y-ofD0X<94vJPkqw0;Ej;__;Zb$bj0NeDH& zte#^Xlqn|=)5f5NZtH(!(|~9HdHav0+US}vu=bcOvWl2&(La2{b*a|=uNyxQp*9zg!a09fJqk{C$pISh=8yXs_ z0Y>42E<(_y@@W+J62@P-T}BE4M0-IWTylq9+Xbl#-ye^C;4lV@MBeai%TRGyS^QxH zP!xjjgh8~t;L(UJ*TlhZ)WJZ$y^T$Eho)7(ou36%cFOVZfj%z;h7UT#UGy8ZlKBUr zRCCgQ0t9g2v4>e%FB)%LyH>&!3XJW8=;)8oM7gj`Ou>jdiOkK;s)A%Bby(Gme=6K z+tcnbbznr^jWvLRL5nPWu6uQ0ipS$4+(Ar=M+Shl>5Iw493T8>LduW`HDllis%t}o zG1~q11`dmU)XRtN6_mZLHUH1qDiUa+g(fCA-zih<1{fY%GjtYs0z`qcB|?CXM?1p7 zxb8xsx-bDp9%mumN^Mcj)Oi92=GkJWrs7rM3-kzDEdgN$)C7wC@#PkG@vSMKEFS^= z9!~Iz)s|`GHUo9G`pG<43tE70l5BFpV&B89o`mUUWzNpm}3QO`q(atfltv?C(cg7{!a-05YP2aPkfmoN$l~3kOc2Ye?0>!67wsn*_uh3@GfN zFzIASbw5gA5yyDecme6Xqdx{47rS8XC~X7&4aBO0{u9_92tRkZFE=Drc?o@)oy|3O zvvii`gY1bCTM#O)`cEX@?8EWEc{ogP#$Vq5!V7hi?{o|d z>R^F+5S(s2SY@8QMOp#J`S^W&e0Crm3xDqOo9&=NncD50orTRPK?duG{#>%RnijuJ zeP4lNcF90A8PB|7@9>jtn>hoF9yEM61BeG+2LL5eoW_wjjWA#g|I^@aIaPlLr7l2V zh%3nQdpB-rmI~z{7sRxt!@d4PXu=_ypRAPx+8We~P+-l!fELsWeId8tAkrQvBFezx z^WHxN^*6A4oghkJn3)B)ePbQ*-x{#N2is_y%#kmvYO@g1BjG>{Cp3B;U-8xNofPeX zp`u4Q^744ml*h literal 0 HcmV?d00001 diff --git a/Logik und Logikprogrammierung.md b/Logik und Logikprogrammierung.md index 378429e..9ec64ca 100644 --- a/Logik und Logikprogrammierung.md +++ b/Logik und Logikprogrammierung.md @@ -565,16 +565,16 @@ Eine W-Tautologie ist eine Formel $\phi$ mit $\varnothing \Vdash W\phi$, d.h. $B Wahrheitstafel für den Booleschen Wahrheitswertebereich B: -| RL | AK | BK | $AK\vee BK$ | $AK\rightarrow BK$ | $(BK\wedge RL)\rightarrow\lnot AK$ | RL | $\lnot AK$ | -| --- | --- | --- | --- | --- | --- | --- | --- | -0 |0 |0 |0 |1 |1 |0 |1 -0 |0 |1 |1 |1 |1 |0 |1 -0 |1 |0 |1 |0 |1 |0 |0 -0 |1 |1 |1 |1 |1 |0 |0 -1 |0 |0 |0 |1 |1 |1 |1 -1 |0 |1 |1 |1 |1 |1 |1 -1 |1 |0 |1 |0 |1 |1 |0 -1 |1 |1 |1 |1 |0 |1 |0 +| RL | AK | BK | $AK\vee BK$ | $AK\rightarrow BK$ | $(BK\wedge RL)\rightarrow\lnot AK$ | RL | $\lnot AK$ | +| --- | --- | --- | ----------- | ------------------ | ---------------------------------- | --- | ---------- | +| 0 | 0 | 0 | 0 | 1 | 1 | 0 | 1 | +| 0 | 0 | 1 | 1 | 1 | 1 | 0 | 1 | +| 0 | 1 | 0 | 1 | 0 | 1 | 0 | 0 | +| 0 | 1 | 1 | 1 | 1 | 1 | 0 | 0 | +| 1 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | +| 1 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | +| 1 | 1 | 0 | 1 | 0 | 1 | 1 | 0 | +| 1 | 1 | 1 | 1 | 1 | 0 | 1 | 0 | Wir erhalten also $\{(AK\vee BK),(AK\rightarrow BK), ((BK\wedge RL)\rightarrow \lnot AK),RL\} \Vdash_B \lnot AK$ @@ -625,12 +625,12 @@ Sei $\phi$ beliebige Formel mit atomaren Formeln in V. Zusammenfassung der Beispiele -| | B | $B_R$ | $K_3$ | F | $H_R$ | | -| --- |--- | --- |--- | --- | --- | --- | -| $\varnothing\Vdash_W\lnot\lnot\phi\rightarrow\phi$ | √ | √ | – | – | – | $\varnothing\vdash \lnot\lnot\phi\rightarrow\phi$ | -| $\varnothing\Vdash_W\phi\vee\lnot\phi$ | √ | √ |–| –| –| $\varnothing\vdash\phi\vee\lnot\phi$ -| $\{\lnot\phi\rightarrow\bot\}\Vdash_W\phi$ | √ | √ |√ |√ | – | $\{\lnot\phi\rightarrow\bot\}\vdash\phi$ | -| $\{\phi\}\Vdash_W\lnot\phi\rightarrow\bot$ | √| √ |√ |√ |√ | $\{\phi\}\vdash\lnot\phi\rightarrow\bot$ +| | B | $B_R$ | $K_3$ | F | $H_R$ | | +| -------------------------------------------------- | --- | ----- | ----- | --- | ----- | ------------------------------------------------- | +| $\varnothing\Vdash_W\lnot\lnot\phi\rightarrow\phi$ | √ | √ | – | – | – | $\varnothing\vdash \lnot\lnot\phi\rightarrow\phi$ | +| $\varnothing\Vdash_W\phi\vee\lnot\phi$ | √ | √ | – | – | – | $\varnothing\vdash\phi\vee\lnot\phi$ | +| $\{\lnot\phi\rightarrow\bot\}\Vdash_W\phi$ | √ | √ | √ | √ | – | $\{\lnot\phi\rightarrow\bot\}\vdash\phi$ | +| $\{\phi\}\Vdash_W\lnot\phi\rightarrow\bot$ | √ | √ | √ | √ | √ | $\{\phi\}\vdash\lnot\phi\rightarrow\bot$ | - $√$ in Spalte W:W-Folgerung gilt - $-$ in Spalte W:W-Folgerung gilt nicht @@ -982,15 +982,15 @@ Beweis: Wir zeigen nur die Äquivalenz (3): Sei $B$ beliebige B-Belegung, die wenigstens auf $\{p_1, p_2, p_3\}$ definiert ist. Dazu betrachten wir die Wertetabelle: | $B(p_1)$ | $B(p_2)$ | $B(p_3)$ | $B(p_1\vee(p_2\wedge p_3))$ | $B((p_1\vee p_2)\wedge(p_1 \vee p_3 ))$ | -| --- | --- | --- | --- | --- | -$0_B$ | $0_B$ | $0_B$ | $0_B$ | $0_B$ -$0_B$ | $0_B$ | $1_B$ | $0_B$ | $0_B$ -$0_B$ | $1_B$ | $0_B$ | $0_B$ | $0_B$ -$0_B$ | $1_B$ | $1_B$ | $1_B$ | $1_B$ -$1_B$ | $0_B$ | $0_B$ | $1_B$ | $1_B$ -$1_B$ | $0_B$ | $1_B$ | $1_B$ | $1_B$ -$1_B$ | $1_B$ | $0_B$ | $1_B$ | $1_B$ -$1_B$ | $1_B$ | $1_B$ | $1_B$ | $1_B$ +| -------- | -------- | -------- | --------------------------- | --------------------------------------- | +| $0_B$ | $0_B$ | $0_B$ | $0_B$ | $0_B$ | +| $0_B$ | $0_B$ | $1_B$ | $0_B$ | $0_B$ | +| $0_B$ | $1_B$ | $0_B$ | $0_B$ | $0_B$ | +| $0_B$ | $1_B$ | $1_B$ | $1_B$ | $1_B$ | +| $1_B$ | $0_B$ | $0_B$ | $1_B$ | $1_B$ | +| $1_B$ | $0_B$ | $1_B$ | $1_B$ | $1_B$ | +| $1_B$ | $1_B$ | $0_B$ | $1_B$ | $1_B$ | +| $1_B$ | $1_B$ | $1_B$ | $1_B$ | $1_B$ | Die anderen Äquivalenzen werden analog bewiesen. @@ -1205,7 +1205,7 @@ Nach unserer Herleitung folgern wir, daß das Teil $A$ heil ist. 2. Wenn der Algorithmus eine atomare Formelqmarkiert und wenn $B$ eine B-Belegung ist, die $\Gamma$ erfüllt, dann gilt $B(q) = 1_B$. Beweis: wir zeigen induktiv über $n$: Wenn $q$ in einem der ersten $n$ Schleifendurchläufe markiert wird, dann gilt $B(q) = 1_B$. - I.A. Die Aussage gilt offensichtlich für $n=0$. - - I.S. werde die atomare Formel $q$ in einem der ersten $n$ Schleifendurchläufe markiert. Dann gibt es eine Hornklausel $\{p_1,p_2 ,... ,p_k\}\rightarrow q$, so daß $p_1 ,... ,p_k$ in den ersten $n−1$ Schleifendurchläufen markiert wurden. Also gilt $B(p_1)=...=B(p_k) = 1_B$ nach IV. + - I.S. werde die atomare Formel $q$ in einem der ersten $n$ Schleifendurchläufe markiert. Dann gibt es eine Hornklausel $\{p_1,p_2 ,... ,p_k\}\rightarrow q$, so daß $p_1 ,... ,p_k$ in den ersten $n-1$ Schleifendurchläufen markiert wurden. Also gilt $B(p_1)=...=B(p_k) = 1_B$ nach IV. Da $B$ alle Hornformeln aus $\Gamma$ erfüllt, gilt insbesondere $B(\{p_1 ,p_2 ,... ,p_k\}\rightarrow q) = 1_B$ und damit $B(q) = 1_B$. 3. Wenn der Algorithmus „unerfüllbar“ ausgibt, dann ist $\Gamma$ unerfüllbar. Beweis: indirekt, wir nehmen also an, daß der Algorithmus „unerfüllbar“ ausgibt, $B$ aber eine B-Belegung ist, die $\Gamma$ erfüllt. @@ -1271,15 +1271,15 @@ Beweis: Endlichkeitssatz: es gibt $\Delta\subseteq\Gamma$ endlich und unerfüllb - $r\geq 0...$ Anzahl der Runden - $q_i...$ Atomformel, die in $i$ Runde markiert wird $(1\leq i\leq r)$ -Behauptung: Es gibt $m\leq r$ und SLD-Resolution $(M_0\rightarrow\bot,...,M_m\rightarrow\bot)$ aus $\Delta$ mit $M_m=\varnothing$ und $M_n\subseteq\{q_1,q_2,... ,q_{r−n}\}$ f.a. $0\leq n\leq m$. (5) +Behauptung: Es gibt $m\leq r$ und SLD-Resolution $(M_0\rightarrow\bot,...,M_m\rightarrow\bot)$ aus $\Delta$ mit $M_m=\varnothing$ und $M_n\subseteq\{q_1,q_2,... ,q_{r-n}\}$ f.a. $0\leq n\leq m$. (5) Beweis der Behauptung: Wir konstruieren die Hornklauseln $M_i\rightarrow\bot$ induktiv: -- I.A.: Da der Markierungsalgorithmus mit „unerfüllbar“ terminiert, existiert eine Hornklausel $(M_0\rightarrow\bot)\in\Gamma$ mit $M_0\subseteq\{q_1,... ,q_{r− 0}\}$. $(M_0\rightarrow\bot)$ ist SLD-Resolution aus $\Delta$, die (5) erfüllt. +- I.A.: Da der Markierungsalgorithmus mit „unerfüllbar“ terminiert, existiert eine Hornklausel $(M_0\rightarrow\bot)\in\Gamma$ mit $M_0\subseteq\{q_1,... ,q_{r- 0}\}$. $(M_0\rightarrow\bot)$ ist SLD-Resolution aus $\Delta$, die (5) erfüllt. - I.V.: Sei $n\leq r$ und $(M_0\rightarrow\bot,... ,M_n\rightarrow\bot)$ SLD-Resolution, so daß (5) gilt. - I.S.: wir betrachten drei Fälle: 1. Fall $M_n=\varnothing$: mit $m:=n$ ist Beweis der Beh. abgeschlossen. - 2. Fall $n=r$: Nach (5) gilt $M_n\subseteq\{q_1,...,q_{r−n}\}=\varnothing$. Mit $m:=n$ ist der Beweis der Beh. abgeschlossen. - 3. Fall $n Definition +> +> Eine Signatur ist ein Tripel $\sum=(\Omega, Rel,ar)$, wobei $\Omega$ und $Rel$ disjunkte Mengen von Funktions- und Relationsnamen sind und $ar:\Omega\cup Rel\rightarrow\mathbb{N}$ eine Abbildung ist. + +Beispiel: $\Omega=\{f,dk\}$ mit $ar(f) =1,ar(dk)=0$ und $Rel=\{S,LuLP,AuD,Pr,WM,J\}$ mit $ar(S) =ar(LuLP) =ar(AuD) =ar(Pr) =ar(WM) =1 undar(J) = 2$ bilden die Signatur der Datenbank von vorhin. +- typische Funktionsnamen: $f, g, a, b...$ mit $ar(f),ar(g) > 0$ und $ar(a) =ar(b) = 0$ +- typische Relationsnamen: $R,S,...$ + +> Definition +> +> Die Menge der Variablen ist $Var=\{x_0,x_1 ,...\}$. Sei $\sum$ eine Signatur. Die Menge $T_{\sum}$ der $\sum$-Terme ist induktiv definiert: +> 1. Jede Variable ist ein Term, d.h. $Var\subseteq T_{\sum}$ +> 2. ist $f\in\Omega$ mit $ar(f)=k$ und sind $t_1,...,t_k\in T_{\sum}$, so gilt $f(t_1,...,t_k)\in T_{\sum}$ +> 3. Nichts ist $\sum$-Term, was sich nicht mittels der obigen Regeln erzeugen läßt. + +Beispiel:In der Signatur der Datenbank von vorhin haben wir u.a. die folgenden Terme: +- $x_1$ und $x_8$ +- $f(x_0)$ und $f(f(x_3))$ +- $dk()$ und $f(dk())$ - hierfür schreiben wir kürzer $dk$ bzw. $f(dk)$ + + +> Definition +> +> Sei $\sum$ Signatur. Die atomaren $\sum$-Formeln sind die Zeichenketten der Form +> - $R(t_1,t_2,...,t_k)$ falls $t_1,t_2,...,t_k\in T_{\sum}$ und $R\in Rel$ mit $ar(R)=k$ oder +> - $t_1=t_2$ falls $t_1,t_2\in T_{\sum}$ oder +> - $\bot$. + +Beispiel: In der Signatur der Datenbank von vorhin haben wir u.a. die folgenden atomaren Formeln: +- $S(x_1)$ und $LuLP(f(x4))$ +- $S(dk)$ und $AuD(f(dk))$ + +> Definition +> +> Sei $\sum$ Signatur. $\sum$-Formeln werden durch folgenden induktiven Prozeß definiert: +> 1. Alle atomaren $\sum$-Formeln sind $\sum$-Formeln. +> 2. Falls $\varphi$ und $\Psi$ $\sum$-Formeln sind, sind auch $(\varphi\wedge\Psi)$,$(\varphi\vee\Psi)$ und $(\varphi\rightarrow\Psi)$ $\sum$-Formeln. +> 3. Falls $\varphi$ eine $\sum$-Formel ist, ist auch $\lnot\varphi$ eine $\sum$-Formel. +> 4. Falls $\varphi$ eine $\sum$-Formel und $x\in Var$, so sind auch $\forall x\varphi$ und $\exists x\varphi$ $\sum$-Formeln. +> 5. Nichts ist $\sum$-Formel, was sich nicht mittels der obigen Regeln erzeugen läßt. + +Ist die Signatur $\sum$ aus dem Kontext klar, so sprechen wir einfach von Termen, atomaren Formeln bzw.Formeln. + +Beispiel:In der Signatur der Datenbank von vorhin haben wir u.a. die folgenden Formeln: +- $\forall x_0 (S(x_0)\vee WM(x_0)\vee Pr(x_0))$ +- $Pr(dk)$ +- $\forall x_3 (S(x_3)\rightarrow\lnot Pr(x_3))$ +- $\forall x_0 \forall x_2 ((S(x_0)\wedge Pr(x_2))\rightarrow J(x_0,x_2))$ +- $\exists x_1 (LuLP(x_1)\wedge AuD(x_1))$ +- $\exists x_2 ((\lnot LuLP(x_2)\vee\lnot AuD(x_2))\wedge\lnot WM(x_2))$ +- $\forall x_1 (S(x_1)\rightarrow J(x_1,f(x_1)))$ + +Wir verwenden die aus der Aussagenlogik bekannten Abkürzungen, z.B. steht $\varphi\leftrightarrow\Psi$ für $(\varphi\rightarrow\Psi)\wedge(\Psi\rightarrow\varphi)$. + +Zur verbesserten Lesbarkeit fügen wir mitunter hinter quantifizierten Variablen einen Doppelpunkt ein, z.B. steht $\exists x\forall y:\varphi$ für $\exists x\forall y\varphi$ + +Ebenso verwenden wir Variablennamen $x$,$y$,$z$ u.ä. + +Präzedenzen: $\lnot,\forall x,\exists x$ binden am stärksten + +Beispiel: $(\lnot\forall x:R(x,y)\wedge\exists z:R(x,z))\rightarrow P(x,y,z)$ steht für $((\lnot(\forall x:R(x,y))\wedge\exists z:R(x,z))\rightarrow P(x,y,z))$ + +## Aufgabe +Im folgenden seien +- $P$ ein-stelliges, $Q$ und $R$ zwei-stellige Relationssymbole, +- $a$ null-stelliges und $f$ ein-stelliges Funktionssymbol und +- $x,y$ und $z$ Variable. + +Welche der folgenden Zeichenketten sind Formeln? +| | | +| --------------------------------------------- | --- | +| $\forall x P(a)$ | | +| $\forall x\exists y(Q(x,y)\vee R(x))$ | | +| $\forall x Q(x,x)\rightarrow\exists x Q(x,y)$ | | +| $\forall x P(f(x))\vee\forall$ x Q(x,x)$ | | +| $\forall x(P(y)\wedge\forall y P(x))$ | | +| $P(x) \rightarrow\exists x Q(x,P(x))$ | | +| $\forall f\exists x P(f(x))$ | | + +> Definition +> +> Sei $\sum$ eine Signatur. Die Menge $FV(\varphi)$ der freien Variablen einer $\sum$-Formel $\varphi$ ist induktiv definiert: +> - Ist $\varphi$ atomare $\sum$-Formel, so ist $FV(\varphi)$ die Menge der in $\varphi$ vorkommenden Variablen. +> - $FV(\varphi\Box\Psi) =FV(\varphi)\cup FV(\Psi)$ für $\Box\in\{\wedge,\vee,\rightarrow\}$ +> - $FV(\lnot\varphi) =FV(\varphi)$ +> - $FV(\exists x\varphi) =FV(\forall x\varphi) =FV(\varphi)\backslash\{x\}$. +> Eine $\sum$-Formel $\varphi$ ist geschlossen oder ein $\sum$-Satz, wenn $FV(\varphi)=\varnothing$ gilt. + +Was sind die freien Variablen der folgenden Formeln? Welche Formeln sind Sätze? +| | Formel? | Satz? | +| ----------------------------------------------------------------------- | ------- | ----- | +| $\forall x P(a)$ | | | +| $\forall x Q(x,x)\rightarrow\exists x Q(x,y)$ | | | +| $\forall x P(x)\vee\forall x Q(x,x)$ | | | +| $\forall x(P(y)\wedge\forall y P(x))$ | | | +| $\forall x(\lnot\forall y Q(x,y)\wedge R(x,y))$ | | | +| $\exists z(Q(z,x)\vee R(y,z))\rightarrow\exists y(R(x,y)\wedge Q(x,z))$ | | | +| $\exists x(\lnot P(x)\vee P(f(a)))$ | | | +| $P(x)\rightarrow\exists x P(x)$ | | | +| $\exists x\forall y((P(y)\rightarrow Q(x,y))\vee\lnot P(x))$ | | | +| $\exists x\forall x Q(x,x)$ | | | + +Semantik der Prädikatenlogik +- Erinnerung: Die Frage „Ist die aussagenlogische Formel $\varphi$ wahr oder falsch?“ war sinnlos, denn wir wissen i.a. nicht, ob die atomaren Aussagen wahr oder falsch sind. +- Analog: Die Frage „Ist die prädikatenlogische Formel $\varphi$ wahr oder falsch?“ ist sinnlos, denn wir wissen bisher nicht, über welche Objekte, über welche „Struktur“ $\varphi$ spricht. + +> Definition +> +> Sei $\sum$ eine Signatur. Eine $\sum$-Struktur ist ein Tupel $A=(U_A,(f^A)_{f\in\Omega},(R^A)_{R\in Rel})$, wobei +> - $U_A$ eine nichtleere Menge, das Universum, +> - $R^A\supseteq U_A^{ar(R)}$ eine Relation der Stelligkeit $ar(R)$ für $R\in Rel$ und +> - $f^A:U_A^{ar(f)}\rightarrow U_A$ eine Funktion der Stelligkeit $ar(f)$ für $f\in\Omega$ ist. + +Bemerkung: $U_A^0=\{()\}$. +- Also ist $a^A:U_A^0\rightarrow U_A$ für $a\in\Omega$ mit $ar(a)=0$ vollständig gegeben durch $a^A(())\in U_A$. Wir behandeln 0-stellige Funktionen daher als Konstanten. +- Weiterhin gilt $R^A=\varnothing$ oder $R^A=\{()\}$ für $R\in Rel$ mit $ar(R)=0$. + +Beispiel: Graph +- Sei $\sum=(\Omega ,Rel,ar)$ mit $\Omega=\varnothing ,Rel=\{E\}$ und $ar(E)=2$ die Signatur der Graphen. +- Um den Graphen als $\sum$-Struktur $A=(UA,EA)$ zu betrachten, setzen wir + - $UA=\{v_1,v_2,...,v_9\}$ und + - $EA=\{(v_i,v_j)|(v_i,v_j) ist Kante\}$ + +Im folgenden sei $\sum$ eine Signatur, A eine $\sum$-Struktur und $ρ:Var\rightarrow U_A$ eine Abbildung (eine Variableninterpretation). +Wir definieren eine Abbildung $ρ′:T\sum\rightarrow U_A$ induktiv für $t\in T_{\sum}$: +- ist $t\in Var$, so setze $ρ′(t) =ρ(t)$ +- ansonsten existieren $f\in\Omega$ mit $ar(f)=k$ und $t_1,...,t_k\in T_{\sum}$ mit $t=f(t_1,...,t_k)$. Dann setze $ρ′(t) =f^A(ρ′(t_1),...,ρ′(t_k))$. +Die Abbildung $ρ′$ ist die übliche „Auswertungsabbildung“. +Zur Vereinfachung schreiben wir auch $ρ(t)$ an Stelle von $ρ′(t)$. + +Beispiel: +- Seien $A=(R,f^A,a^A)$ mit $f^A$ die Subtraktion und $a$ nullstelliges Funktionssymbol mit $a^A=10$. Seien weiter $x,y\in Var$ mit $ρ(x)=7$ und $ρ(y)=-2$. Dann gilt $ρ(f(a,f(x,y))) =ρ(a)-(ρ(x)-ρ(y)) =a^A-(ρ(x)-ρ(y)) = 1$ +- Seien $A= (Z,f^A,a^A)$ mit $f^A$ die Maximumbildung, $a$ nullstelliges Funktionssymbol mit $a^A=10$. Seien weiter $x,y\in Var$ mit $ρ(x)=7$ und $ρ(y)=-2$. In diesem Fall gilt $ρ(f(a,f(x,y))) = max(ρ(a),max(ρ(x),ρ(y)) = max(a^A,max(ρ(x),ρ(y))) = 10$ + +Bemerkung: Wir müssten also eigentlich noch vermerken, in welcher Struktur $ρ(t)$ gebildet wird – dies wird aber aus dem Kontext immer klar sein. + +Für eine $\sum$-Formel $\varphi$ definieren wir die Gültigkeit in einer $\sum$-Struktur $A$ unter der Variableninterpretation $ρ$ (in Zeichen: $A\Vdash_ρ\varphi$) induktiv: +- $A\Vdash_ρ\bot$ gilt nicht. +- $A\Vdash_ρ R(t_1,...,t_k)$ falls $(ρ(t_1),...,ρ(t_k))\in R^A$ für $R\in Rel$ mit $ar(R)=k$ und $t_1,...,t_k\in T_{\sum}$. +- $A\Vdash_ρ t_1 =t_2$ falls $ρ(t_1) =ρ(t_2)$ für $t_1,t_2\in T_{\sum}$. + +Für $\sum$-Formeln $\varphi$ und $\Psi$ und $x\in Var$: +- $A\Vdash_p \varphi\wedge\Psi$ falls $A\Vdash_p\varphi$ und $A\Vdash_p \Psi$. +- $A\Vdash_p \varphi\vee\Psi$ falls $A\Vdash_p\varphi$ oder $A\Vdash_p\Psi$ . +- $A\Vdash_p \varphi\rightarrow\Psi$ falls nicht $A\Vdash_p\varphi$ oder $A\Vdash_p\Psi$ . +- $A\Vdash_p \lnot\varphi$ falls $A\Vdash_p \varphi$ nicht gilt. +- $A\Vdash_p \exists x\varphi$ falls ??? +- $A\Vdash_p \forall x\varphi$ falls ??? + +Für $x\in Var$ und $a\in U_A$ sei $ρ[x\rightarrow a]:Var\rightarrow U_A$ die Variableninterpretation, für die gilt $(ρ[x\rightarrow a])(y) = \begin{cases} ρ(y) \quad\text{ falls } x\not=y \\ a \quad\text{ sonst } \end{cases}$ +- $A\Vdash_p \exists x\varphi$ falls es $a\in U_A$ gibt mit $A\Vdash_{p[x\rightarrow a]}\varphi$. +- $A\Vdash_p \forall x\varphi$ falls $A\Vdash_{p[x\rightarrow a]}\varphi$ für alle $a\in U_A$. + +> Definition +> +> Sei $\sum$ eine Signatur, $\varphi$ eine $\sum$-Formel, $\Delta$ eine Menge von $\sum$-Formeln und $A$ eine $\sum$-Struktur. +> - $A\Vdash\varphi$ ($A$ ist Modell von $\varphi$) falls $A\Vdash_p\varphi$ für alle Variableninterpretationen $ρ$ gilt. +> - $A\Vdash\Delta$ falls $A\Vdash\Psi$ für alle $\Psi\in\Delta$. + + +Aufgaben +- Sei $A$ die Struktur, die dem vorherigen Graphen entspricht +- Welche der folgenden Formeln $\varphi$ gelten in $A$, d.h. für welche Formeln gilt $A\Vdash_p\varphi$ für alle Variableninterpretationen $ρ$? + 1. $\exists x\exists y:E(x,y)$ + 2. $\forall x\exists y:E(x,y)$ + 3. $\exists x\forall y:(x\not=y\rightarrow E(x,y))$ + 4. $\forall x\forall y:(x\not=y\rightarrow E(x,y))$ + 5. $\exists x\exists y\exists z:(E(x,y)\wedge E(y,z)\wedge E(z,x))$ +- In der Prädikatenlogik ist es also möglich, die Eigenschaften vom Anfang des Kapitels auszudrücken, ohne den Graphen direkt in die Formel zu kodieren.