yc}({?>?|m˼8|6 p바 Mc;{ ?-4eߣK; N,O^>%}8UѾ껿//I6 o}9ki ɛecO~F[ZJ`4:˽푡DY y|0iެ{ӆmⴃ}G3d Fwo |zp&ߛϬߧx<4Z }hϚ}M7~K [`yP^+[}{{r$J#͑x 28s=XW.CM"g/)~t9'A1
i[O?_ 燿M/.~
Z}ko{xjOjX:`zb4'<^`O]ab6\ .49So's+(i7lP.Q!-lC|M(ն|.%-=NmvIy@$4OG7%Fk2x}NB4M=͡gŔXUjSElk*Gɢ {(el
tUkOC)h-z$rZktXm|i&ax3 Ce VR&I'4(hw*I( s_[ob4۔;b}sa]a'/Cͧ_\HsV,x6 5bm4W'&3EjumƆje;5ʣEtl`mA%6]`©%u̢O
apM0]TІ*]Mx^
s٭_ bS:c\5̷0_Z9u} ]4T1_nڿ1/rϵhϤ\EɮlBHƘ2ILg8 &C
#aJs9)k-;s9Uȁ [AN1
ޣGdƥ8cr}sT
A+G?i1o
2mmC#2)b@TbA5%,(4l eFT&vװ`^ʃ dx\sUk Yl:>1i$iS#veAMMG=m8),2!) rO>e-l@
A}Y; +e0K*Oe_8EawlsEu $AhCf@ 茟E{_<љ-Ne!6=Vel AsAVԜDjͬ*YH%l H4.^ZJ{ʚI`{sdBy 붙Pf[쇷hmqcv.qu#XX2 ͨ dl¶j&`~߅㺴ѵL~?w$(BRđ7 &/X:QX[oD e >xIG aq}ĈLGpq~aP| t6HJ7ݖk'f
Zfne_Z VdlLҋ})wʮKְNb.&9vǹoXBY#峆 Z.AyepjcUb*D1jL x+5E
-J뎱%JL+B
>J ЅTHe)p,b]:b*10s+(jj K&6QZd?1Q5fDAK%-J ˦PvS
`<`IvFBVvT5|%2MPk`]=lMF݂@,9ȆwUG$UQڰj:MW(H`q5dl`l\k:|k:Edc+ 5HM5
k/N+
NlzS~Wt 4 7}}
Enʚq"E?F**ZZ"&KbNhPR*MlVSZ-6杽[ 2E@ ~naUj7,U]
aMCJtvsb)w[@d,͢ekT7ZעM ET;L$\GB
JzqW5)bՊ!ػVgW|V(gauY
Oɔkfj9_ V8t_Mg(Ҷ#3&<-VjP/C!@32^lŘqpZ5- &uָuڗ#WcՂ핫[%eu
$& b7s/5hǑoҹe-JfJT&hXl0U>~^gm(8e'bFt%wK'G0mvpBOuڢY0z7<|+7tbB}ywĢ~P MZv4=Ӻ;zLʲ{tPҶ}ʃnHCÞ-e+6 jE".IYᄐ|-'-;fpϓv쩫+YMjMsr2pX;P'ZMȒB> ֔PA)RT *`:dˮDޘZ?Q|f?&糍,eJKDIlC}ozt'˶Q U=*P}r$}"aU[sR䔤%/?Yy7D myr٭IEe'hofS!\m^MQ>_>IF^c*a ާ^vSl{]Hb_k;H`1X 8
"H+HC W`Zщ Q}}tN1g #ړ`&{JlU O't9-uV,5zrC l蚾*孥Jc =7KդD&G= -l;VW *0UٳMܘ\ ,3yy;[!MZ/g5"
M}U))ODUþ qQ}7Oκx&,#֎E=:M:1U
I[RIݒb2W gRws98sz>v0 0.-% HgAsj4a,$1 .RWh(
洔ǑF(iqB;Eɒjq9
wD[&^Gg :%# 0魳1V鍬Ҷ]&Ĺ L̲nG GG#䣡mg{2@ڡnrR`Qogkm89x΅&%%ltRb M;}aͯ¡LSwVJQ8 NbEKex
NN
c^n N
C[e)+WV ug5^Ja#.+'%pIL8iV]?pUmbmђiHo%n2 ,bHUu2D;AM>".ܬ+t w1V49)4#<S,f. L7LU{w>6f>)ko8vpf;z-(xH;k gKTXC\oLg?u
5m*GTezo xb j5Ų 'Cjj!>3g?A |aԪ3#U0Gz3ڜxi
TJYs/ y]> IļmQo!T6'[VLXڒ5 iW~fR8&'R]òE +k5~^>/7&u*:_בkcg] l] hs? LKeuD6oIq;kۦۅۙrZå]X$ /
L: lM$d~| K]=6G懇Q U /ESa9
Nʥ(ڱ !kaluVuAO g
"X
,HPê'ՒW&u `0|ܐR!zV W[*J=6fFpp
< .@s"< 'dS"?8^ (+}Bye&KNzxEWX{M gBV`( V(ZyISTgJ{zRRw f(Յ#Tʢ[kxqpKN! W@ ދp
|9a@Z 0#tRbz` +aUc\Z)P7T@)SxJZe֜c7u)"l+S;A0JY1ˮ[uǛ_ct1G |dLڔAݦŢ5,ee <.Ӓb W"q *,iiAUEK*pN:}`n={U۪ T[z{GJY*pBT骛 V HRW9lje
doÑ
$7 `IJeD 9Zꐮpi-`oNbTEԖ"y!u@UmEѦ%keM(mq: q$zIsk +R
۫ ev>J Nvľ# &wf:ƍ ljSf26%8Z1!嚀XnP
c&|R&C5 Ro!8պi `( K
bh !* NpYCA犸W
"FHlqU $/Tb#-A/Ƀ)0)`
+#355 p22PecPmgI]= .?7ʢ 7u%t.*Y[bXPk
`mC[xۘmQS?\X۬9O ếp1]-l\*Ya52F)d
YeUȀypԩe I@TS KD 1ή*XCh`LM/!)Vy'Z7
OQe)yf4#hT! R/ZvV R c 7
3A>kH \J5E[B Zo(BtzwLT^WL-_O%zD#^1ULkMGNK%{s
-cq>&>=Wی]j L>%@jdwa}DwT_tS%ȢN -WScY/!:n6զ-ƥ+Gl@r U .t;EU)+`I*";>9Wo;$W.
ɸP#1+9 )ÊR W |Il{"IHkH>ւr.@F }%0[5@h൫O=' VV|R%',KGHP8d]*WA4 N;Sh ߨa@ J}&0KG-l
^8hGhzX dƛL$<Nr. >#eKCnfR''c/R Wacv-sȐKUj/`IxMcJ#4 x41" f$SY,U]8mHʄ$,0:x+/y"HE+*DF[6
2_O]B 纾&+D[/4LXo,^ɻ3-{;Cu>SUP.{Vo. c'rƹSCٰry u9&zƝ"ez;KnWFog~8Wk/ kcjR+7+Rkt
rB, ] ܘ)FBB3ĜJg à*fӗ
ۅ7$r`
HF2gL*o M}u&G7J ;"@^3'9_I=SW$WՄ#Q]oST~Se{Umrw+vy tLTN6i CPGR@ftM匂 \̫شUv\A!rPT^7hh+#Dt&Fuqbsʶݽ
U;+MXIlSgtC\f>Q"Bڒ A7 Q wcDz9~9A!) '=x/8/8zˎ Nۣ÷YiQ'UĽ>b}slJn->J)dp| DO $
̵"a 3CK ]|(W_Du52̦e?&-_˗DCǀ7IuU8q(!r&7z(4,1_Pu2f`wm?8S#v;D1 ?֙ Z(X0EfU=,(^Qgs +ag k.gB1I_7^&39l!+x*j03_&Ezk=Bae @_5f4 uhXS$աeETc6LqWu_/$Ekn>M@m䴚Nn,%+ss^r9e 9}(]pIB:%p"~e= 2>K;WmX F'SׄU_`[, 6 xpR t7*@C )9*LTy n( L9X %^[w:p2R `БI$*H\IMk (UE\%[I|
b ygx0 L I-DKýKqܾUƷV {kadRMJSMF1$O>xmP5n 7ܳ2P_8ƴ
b:'1"&zT]f I^ #MV%״%:+`1V) դ ]N Wũ "V&D^~V _:tI t#T~n+NX X Yq/kk/; 7h cRNYjH r|A/Xyٕ܄*Zt*n8^%| ,ᝧNkz'7wu&|Zq b&nhbfu0}MNZ9a[]ox
]]9ʼnqvvTybմcQd/Wĺ7 4fFǥVţG ުG(ij r3sWddXnib/jM( U}A'>_G9G]6>\ݺqAj
3; K+z (D7zgod"B/Nf0Ɉ&zf% \NGhp|z1[XJıȬ<: MD c|+Z ! SR,Bhzh=&`$j1nqUZQNDXZ
9mA
EuDsNyi QfE$&M6W^-H£^(R*ΐ1,xD
m%.Ĉ0lV!A`q|N '^6|'%G ռs+E^&AڂX#aHH-(+-m%eB\LJ*2І7p (D3tT s XvYK.km٪hނ,="=;
JAUA0UFy
NJeF8QNLFcx HJ\Zm"KB
D|q5z KL= ]ĵe[4-fJ 42 u w)[gw7FZM*AYu U/B~D=r z HO{h wK=\ԣVJxHw0jj M)։2efMEHh$LvqK'FcQ=W[}Rmw @qTK
hښ(
q}2% SZ?@2zpi 0
Ȉ`x":̍즲`4h-,'鹄
R ųQ)x5_H
ܦ H%/GR9D7 ?]&"d70ӓ),n]!-FjU d "٩oDH?c;FJPD9^(QI@M=JCz4 k!܃;܍ȂvqE0^I품"L@YpPU<2>9_7SEfFus#2xB1 )urF^2G9%*W1(/ybi=Yo*LÔEPj΅[#RUJ";1YI ]蝚5T,ﺘ)HQ:Ar-S$%L:s~/#ɥxFff M5n\KT.ׄzd "5T&JN!26dWϫW Ȫ2i:n+d/RLɼMVM <DROBQ?3K 0 X r $eb:i
:xTIuB\0Y\1@D rHHP۩&\bL6] iIrG^U|fh |陱+dW=qL&Jl))rC2x$>8xΤiW*DU9D`~& S2pU&T j!DT&K#f# l&uNOm El ۩L9[FO-`܅S`EyBHٖ b`VRCM.Qt$[c>W'R $QxApxK&]Fe%b8VW^!Ä0(TJ`6SzOzζ)*T ި10O[(b!O9 .yv)Ay( [E]XPMX$ٰ :@ DLAv(KX<(-w$zIuelVn ^2Y@_olU bvIy S9tiD+VXUfaVa`6wpӌ-lF:"z@Qӡ i$(VZfxŭoN$|¾>{Xo.TB|kaLo=g5`cD~ֈi8&cx @ @ !C⏞W j2<gROwa퓺 )_ħT*;$' jNPqA gHb1L$1#=ѣgBu c Pj9yoYM$) GPkq|'c! `R-YiE ;y < HgL! 8h/I (ZY]Jhh+zIo"T51MFKgnE\~doVyD@>IyUzg Udwˠҗ+fFA䃱TxT\i 4@ <"
@z@ v'iGCD_ Fd8H gfq`jBJ ̮Ӂs!F5oĶȬ7i VU{#d 3Uh۠Mw9N`2{LI3 \71p
UNOq"B4nx2YF#ϙ>FA[<./y鏠%fxT[
Ѧc[ԙ[S$y&5vzM(vχPKA3Ӵ/f#K\y!K=#q+ Hgn$ )!ή{ዟ%gnȕ*bnĔ \~dth,~pw~G X+*
nFV(瞵j UmFsgmYv O 9:{RI?vkO }dAb`M
6IR%tIxyJl10\Ԫ 1-$fIO{^sauғ"zal.^#V]/]֨Ds A爔(q QcsD :$$[X_I/M Hpkٞi SFcCRQ}TKW)CR>w?Kg]\TU@C gR+Ml XTᩉDS5ճ1@7pil ȡT)USg%6ƀIjozV2O tX(${|fܢZ^s|LLmNOA#w+qd9Yq
JD>#7-╸"J[HB *4!;Ku뎉HSΙ7 -1Ј渗1JOhW
*J%ORE&B A2y#RЊzY"YX,*M_t6LqnU߰9ۘmh"B .@ag8+L4bMYu+j; 1QO̩YZz_Mct}^qM`U0z/o$E\rl;/"ŗWdPG*7-`HX&l."XGIuXn.zy4=Gs3\RV}s)v9bJEsq
$7E_8֛ދ x&V@lwK Ҕ3KG4 tuk!=~
0&:!)tr^bKz&6р.1,b'"Lhv|Aިy_U
C6c!/Jfp+{"ԉhh^U 56hjƊ4V*1-Lu461=l΅>#Hfi ' Yİ9bU/9 MCMK:¨/~菑(jTf, $A!FԍHq'Ӵұ;VwC5: h)yz("9C! _dn+b7e=Ꝥ`&Q&LI_a E{SC ܞ }.S>vuߐ &gu ,{Mԓ*/G&YY*Yn#JGm C2|J!6Y"W8(އ^vK 9+= wT펆Uu4sPQYC =BX &hX
iҷiȰݓcM_{T;YU<6sARdjOm+Έ^γkVg( S
$j¯-1L
da6sd˕e!0u[^\aI]],}0J%({?hŕBT$stlj́ @z[_;Muu!d
^
v`z |^/ Uj]w eEQJKғ笑P+!(KKMw >Gĝ26Z?и1zX.!VB`?_0|QA
sGcȥXVȠh V/@I _`<$]lv{YPHʝt)>Z*As0AnA</8|x, ]]E#H!vt}S7;J" 91R^|qA2TapC= ,טp NAF } ny)rϢhͺ$nDU?G`LC
YOGG g.= )utd4eE:`5Q~j].(9a弑."LR]^iZ1H$Q/
?H:BHוz%Ҧ N +&ؒؖ/?$1Ið A$#%VH!i_ԋ&җRRK4=fU^90ԤP(9mC j4p#r& 0QfnQ+r/]
sg.3&X
8D`+ E4]&1J/
?Ue N Ez
84ubVɖ%PMpX
8\+)2-g)IqgQ-sN#~̡9ğBήߊeu?`rnwHn9`G:cwI._"(DYNwHg'0'. !܊0uB_fY *?H ޯ>hj -$pS"7, hRZ8ܠ <~Ro&n&LPBHY%F NGiHI R~
$ GG,@՝* NbN* 79l*mzTNEL^|ԝ"S8R2ɏ7E/.Q3C^,e`Sd V@Z-/ebdYQ1eVF?،RT/8C4t
3 Q#٩E%͝=W{._0[N5N< 8AbKJe<?4 CԿQ.'b%']:oGދ}!lދ⽈;15m^ ދEPs]mas^ąSQʋ "z#0Vׁ1p%xe
<=XU"Ax%
^,T[!dh$S沔A :ӫV vN^C 7,~jiqq=x2Kt'"'t=& >8y=3
n ƬAfqĀ7Iqs= zp> /&eCVJ7Ϩ ! UlnTb* ;MCZʉO bUz^ 0i* |=d4ڐ{bI\xM\ rS%$)@7-}Yi!胴||k· '#>.·yШ7YFcZˤ+c#
6י26LD&5h)Zܱ{^3 qd4LnNk&NG ո;[Gˤ(zi'ɑ,%w0!"]M "[ ¿D5V[V#&=m iva >&Ji嶻k#3E FXgd_W<^ %E:L.q j k=h~K>l|3M*|Pxه$ݕvHQ(Sǐҳ2k*]qA/,+8EdTQ&%֒` #Dh o2{4
4FDbi{-d qj{
i&
v0)HTO &w{\KҖ4#&#g^2l ;M;
9?lHrf%Yh6sQYȮ֎: e'qu::''mfft +lj3yA425$m) ѐ#f<UB&a4#nlA=>ؖyG-yOl) a{X 9~zYvI4ʛ,Tq5#/SC䪏V 85}r oFR h%;9[O/i)!Q94N
Ϥ8@%#DU5 yLȬ V3*" |h2Ahz" w:⽌R<(%#SA&Igx2-E#Bexj)S%x%@|X|P5;LlQ0QE. B+JzqDx9@#2!A`dp ߁$q[ iX&!}pkK `^Ο{@;I =6_LhH /$Mþ
zt0ao%NU)Rez
P' Vyƕġ k9(Ȓ,n輇.W'{L_1R?xx<@wY⃡:MSVfn c J3C C&zFt@~Q=$J# @dQRodd+'Gu = 5: ! =eE75Ǩ1i;dwEYRPԺJ
7 ?y% H0KxP U#3 hFF̗mF`1\Z
=݀I@" lV
".l@1=]hpBL0 +5+PjdDLӬ +1!dD8>'dA]
Fa!=\ w8a|D0SX6 H``"VP>̙`6K08픬٘5 @ nI iGR݀ Vx.f+q;F
!1 R1S)[ \^+%(A0 0u*m/Vr_k_(jJfxZ+=Qĥ9N
[{0X$]X
N#r 4)"Gllg@ ɕ $ 77'(2 {x vVF4 +W$
h"5X(RqKrÉkbIYLUN%* R-~+S m=.gDq8?04<SPhf& c4YH4ee$pF K3vĻK Q[m@5$;YaE.$ )^GT]g^$5Yn|-u":
l+žY )L\q(Z# ݐs4@38/bj-W,`:M."ɧ\4i zG֗+ے#%EѨPZ}y} yK貾yrAbpOL&{{k뱬vn#^gD$]xJ 1(?~(1W4bvJYTz=s>(ٌc%^Z$[ZXhg驐O_ۑc4wAΉÍA=8z[!r5eYw"ƫIZXVPS ٟբr]si:TY.b
+b{ $c {W:c|,=RU_T ˕}V5Z)^ߖ 61gJĿGN¦zK1&{[-pd/IZ@,d u ߖ4@!0]bp"۹@CB][eEGU1־ȿŢmx1:֪*e۱"V-5
狈̶o+$b8 2λYv
+C#"{*Jrcqq=,U_KIqh)~3O&nu8jP"i
߽WYzu*I!%%ƒa
bѣY5l>ز6M`˱6n[M$䲆kXhXӊI`f# ԝvќR3+MA#:c۫eVV>M鰔/b Fm'jUXS,]3Eg5zs3W_GyH 9Z$uzMFL7\_jIIB#ŤRٲj8Ne>iŨsQ\#╫*(+"Q<
lewJ/@z`"^D= +M z A$ek62Yqsy `sU
6&_JgFڈK ViVJrEV:1 `nS@1h\KQ([ -b!G{]|ՖWf,\@r'HΖNWmOnsƯ@
s!Vt#G]wpӉ nY4Cg˕Uy tl}mpꯠ2bl2]F&5'w) o#d`uveHbb rάn5`w
P]̥$ ۃP_g:o8<@㯭%!#m_攍-2Vzk"> Εq)FKb2o 92-4FBIT->'mVV{dQ%[(TK/^rѺ@6 fYZz7ٕ GEٛNE`2jИw1D5R.{fY>;Xץ:і5#RsQoҹUƂ/ g
Gn #* Oc5{_"Fs-=skRŨ#>/rE!cqHC( )5O wꄚI pt*fPQ:&ʖ2:53WX8aH$XToAQ
'Ė!ͨ(N*hq]U[#VZջæ58ފEA:=UܨY[I)2dCRC(X{e&w5 d ]b$LLa)6 5Lh*/S(Z^,+uRz Ҋf| {l %Q3(5^RÜXYA{ BݵH`kJ4XRGL"R|fba5ծGP~V:i)F Dz sI.DZaTj}kpBPB9`إlİ.\`LrQ?ZzI\X@SR0D?c6
mh %0@d͇'I>sϣ3!y@baBCYRFfspQ۪e?b=Sx(ÉR +r2SyD'jq9;;,ĠT e|Ru-uē,/Uo sF0Mҥ4]H3 kN%4\.IV uiDuY%D|Va[C{ZKȇ64zqJjZƟ|Xto)9KEM0 eT1%|^;. - וL=?guZ;Xk6p9?%u((D[H#f}80c:LK$HҠ>H3gc50nu Z{ڀV̠^M'&5SLw4A)#{Eߺi)# (ԩX_miEj:јiQH # I\9
A/B#r
hu(|"z `._tG":^/V>mv7#I?"6O-o/ISq$^eF?seA h҈W:_vuXM UDZ"Q烁-0BHR86#`<PdvTvH
<ΨnerV՛',fFXYH[| 7,*7}jE}`I'%?;8r($ړ&yua{3A& q3]p) [R"\wt>PʦXc**:^l^ʅtmVu*jʢU\cD|lMVTLB._?M_? ſ?=$U0A"5+PWu21Or0 .K11`
@( ]8{fѦZU.k#*(S7LSfK/!ZꪄlW=m,"K|uF/q^4) w:|[Ydy]7Ν|x
ݷ Y2ްjV+?H< e{N_d $-/܋feyH2z
aK#'>R8/Ģ&/{bWlu^$ V}Hju3_LmfK
D7J2z!*C;Bܸ٤0<,z|4 q7ut^ќJ碔zH,Ĺ-ז F8["F`|oHM,LҲ/6Y" _I5h mܻTύ6=_ FIG$fY.354p>ؔ9 #Op 5Zabd
2Ҕ TV٩`iQQEF
Tvߙ!Ev_hI)|Ѷ_発5$[]ȎÈ?FH,Y&@uF1yaI.
D}(UM6M8x*!O<\b(Dϓjq@]i2@u\ۿjEQYӖNL=7TV{r梯
Qhڎ
ٺZ.oz{8n ?md /I >Cl9 ꒐7S02vcbKQ#6%̊"'Cnq`FH5KHS?/Z#iEΔɵ8yZ{A##nFԵj 玍i_W1d快8PH%UĚIqR>t!2x[l\T|gڣ 98QnFAk*HIha C/wM: 뮬_}H~t$\@ x1}CBw=4bo)f1FkIfuJ %`V!?$-X|kLe'wJ1*3FRW:&"ϒ:V _uxrZ")?\@e
@3k`M {3z \TCN+"=9<*my&KzFOۛե[>]v
k//kx6Uz
o~uE63=@7o4_
wvv 'FT/*H_|j\}l=NkL~=0d[ˣɈtEO F+OUʱahWWUJY9
OQ
/ C}.!JcGDD[bb gҪ+-Ok};P"xyF>˻HG" #[SV%L|tW1CF5Ie _LIo$*zpXCvʭurvQ!1 Yb[JY4(ҕh":.IRݺ45ֺMr}!HcvΖ@>pʠ 0e-)c9>,,l
En(dfmD677axЛm3_ICTy)nrw\2aWoDX XEAv _/$ٓQݽgv~\/j uaJ#ĬbQ"@5٭ h=3U v ju pt+:h
!gb.R'i4%j$(35Dr~ioϴF%`*'xkKffuδѬyC:l*
6І&.!`9dX=/FDeT~|aPHqe?j\]Y ,WS2h&
dŐ~mF T4͔uHIғ/d[J֍`mjn=σ;mZoU]ӂ4G;e WN+J+]5
} z@F-Nʻ{.ce*~RKȲ!¢
Tn ĝ+MnmnSxuت9!·Mj^؆NۙIJE:|u;ګRnk'Ip~RH%
|WT-ߤQT"ļF0%?>ԋ3j ƨ0u[EnOAߛjPv=O=h n(z0^ 5/ 5i"{iE&TRڗW6 `tR)Z:/uUjrFARTܾRCz^$sQn.+Y>K@$,i
Vo8H F!ԿRnjRmg==d
E!hSoWNY ehkEuOX^ZP>/(W A4S|Wx.!$U@PۆZ?)tئΩ6˨Sst0Ké%
6Tpaj59sY"[ΰ[0I ;_[rO OZl8(TE)GȲ1ɘ|Sy*4G7P6n PFt];ND@ UmGAIglH }BP 5х@.TB 'mWv 9kQM;`0xq伫.mUie\5? -
H^ ukHt%p$ c1녶w_^ ә@/#d5
mX]S5X=b,ԍkN 6[e)֞t2,.dujsCYda,p*`n6Ta=YdBT5Rbq6Ki˛HSRP?X49|ÇA 6C
u <ȴ7<ՇQK-}@5#C.K Y"9qӊ.w;7 2 S쑩iŠDwjpj{ \bXTC=u>@ϲPPH\ &۔z,_~Yg,i4#>5aMExň&# 5,W CD6U4'wtb9WmGtP".wx#u#BdnLnVQ&5{d=!m/7 Y$ {&x*2gNq8OQ#!PfQr L&6d%
]SIebsS`^VHٔ=ۄNr= ajg" WVRiDǜ45ʽia=TzG (
Dô72&S㋅'gGvޒ Y}p i P͔RjԽ@[;P~
Yʂ>~ cj;:
`gysEA!eaf$^Ԟ_xL*4لK}z=8H? !R ^±iW)$ |@Tc@v2_4;BX"!܉\G*H KĮ3-be% +-!P=<ȴYAZMu&AQ XL־d6)>C+A ZiR;'>dUYNP1{
bd+ RI401 嫬 r:NzqVI-G|uGԅC Nbɗ~ovp
J(m:+fi9u \(PAG6s` %m@ff*A
'f8ᖅ~I|lA}?CFr ` u Rړ{e(~ɩ ; -M \Y?b=rjB!v`_șDu&s1eE(|,b* '@%oqɩѳUjd TPvWd[ꢏ VpJrpmjQ{=e7cD wp8qxm6';6z'~
ۇw b PؚXF m5R)z mXE.`3H|JT$PN
)iSkXϯ˴UrAot0G̦мH +nΦ6,#ם MB[ݻ$Ȥr۱=PD^ %t1uhe:7OPn^pHSF@ 2z
عPסU%d:|:d%Cg1U.ɔjccWvJ j r0Zyc
:hs"q.l rCS$ oǩ$l*^6# KW ^ ! CY 5E)hjZ)ה!kJ+,w.7+y2hjCuuOZ TZ5ZGR\wu hfQ
3BcUKIR-o
yc!Ϡ' ϗ)U%*oU6b%#=]+5Ż&i &3\ 3> [E)ou}[sXIKeD U#xwtR)SaY .۪Lg&V@8TU'Ob["Կԩ.L^um$#qnij~*֜Q5%JG9iɧ D'a>`x>5"W~nķZ_oY[wV otD+]u e|[\\|C9*8s }4a?,ιZ2*&{T
o)=niH %7il٦1ȩ2x[T ,+(7Fc~V]쨯8M4ЊˢJŋԌ`.ՔC!=W@ zjs7HYK50Q.yv Isܗoc j|۬1., 1Y? f9t>b{ixe0tEs9i "."wF5̮nm7;vP>{Y*Oݬ
y5B#O Ogr~Ζ
;R$Sդqsw:g /EX6.L$Ր yB#Rm*Y K0MnJٹ f5j)3VLS)|lQ(0"O>SD5%3EsA\Ni0lYY5p_$Gfg@ȝG f-rVQp=JJlԺ.e)h"5^PiR.\0%紪1xcVf^[qc%ET*RH d'R62a7GC*y r#9(-1lC#2Wd;uiE*6e\iN(R2YKIf|dwg`&/u AWg!%jY3.nX jJ#擀F^ͥ
Gё<&+t~4Y^غdthEV$Jmڜ_&([u+ S
;!u~ռǡV8Mp^mdMBA|7Vĺ: NZBI
O/2U=)2<\`8ӨZ2 +_
*A<
A%>i|S+ÆR/b긭SI96d$ o>}U^[~T*Ȓ^WS_͗0GˌIO %`*K|)T 4O 拸6BUTf_E%>jj*t@թD(^ EUp[CdأKB3Ǎ#++GZWQj %Z(s]R@sL<=4e*rVfa6T?IQ1!+OJ
K(||-T w0TLOeq( !%YTL7j J_Z?1r̢t(7Gm O+t-yU_%b QolʒԘS+ %| NrFl-U[pjΣ?]k-5;Fʽ*2GYhQ[JS LbK696Q2r2kXX ΠIxa0FL++e/2SUlSBw&
@VFkg`&vrhyӤ?B]?mv; ^OT8 T.~+kB_!SmUg{T`DʯYIaF-FGVj}9+d֮QiTތ>\aQ4M \qWq%oGEJʡAm -{#_)GCV1eƭ@
q$ 5 C"GXC7C^@TD[i,4,3bMe8e5 Q#9[$#d _-IVue+sD-0Ip2xUX_?"GxAKA#*ǭQ].y<6i
1U+ehsr9x!B* W$trflT-I,\$w,nfZd^dpP9TL;YK{t^zVS vKLw$;V{V&k͖-ۂ^ +~Y=W|o^-Sh u K U\D=$J _ɨ5J ܾj!'4Y,UCbM U$oib] ]+;@zHw%bD#яCbZa dBE
Uzk{5,f =TʏY~2 i#&X%nsh q| f7l>@re 9>Fh Y95\W֨1A>rb-0Z5?>F;
!3;Et%qˌH]UOq ZU5%X Nvc>av"6Q aѾ qѳGx=G0WGS3UXO ;ڌBh_H[FrL꼜蜏o%XKA#DɴD ZbO~7C@W
>9<70 X]`!b
ϑB("RЧJ
. ]Ŵ
B|QI O3m֊ UE8=H6!|5nݎW[= %!SF)k`"ɪCi9Zq,DQQ:(.vUIW6CdvU PcQ+a`4Kb<ª# { ?QU"<"MN /&>+x}٬
e $9^maI5eĪVm^m1p{qGu(Roj\,
7M UƠUzՐ!7{r>H ,D`hB
5{_ Έ{gJ?/N}/ GJoy%|N++M<
ucb.dhטJjSǵ.bͺ*_A)'(H=9G o,
8sZ(ə \.W&HqsY刘уY>\*ALӆGHo=W툾ch`G< 0i-Z}0\5U^݅v1Kj/#0ÚuWc)K7[d)]YI+()dZ^%Z]`tI7H#QLBuV#eJyM=Xv/ɤT|DlO$l<zHڊjWN?Uw!ϙK-{"y'dN$דa%_!dQEf=9^4xtg|v[=H;`C]
hA=hvP^ b =8 ,MR8XE@GޣzI
PW/ ?ڻ/N*ٗt>x2N/֛kťEbxjfKI< W ?IP4Xϊ3\m4vRj
(T0ImZțS)CJ=8P&_DUX/#WСR~@ara%,Vysvr^gP٪LVydzw;0nH uÆ2YiU l7Hٟ/ tu9d;;ɚ\@]32M|YVߌ8%L{ث{o͕$g
9R21jO43i&d 6\+{:@۔6t@V), 5`r+_]C;L?.S#˄Lo~UntG O)( Kɩ2z. aV
M&`RLTI =c|#E=l/'eZڷUp]RTJJ 8TB] t{ML `Ee #-W#0@뎎=X&&o7_^C5 V&Û/)^E$nȚD"p90g63"Y'mfue; ,G#i m$RM62p>= J*Pa-Ғ}o:F 2)&5 , ˣD(ry3DNL=ݙ n,;E ozF.!zQ23i}[I 3T(^8~ H|ƱMΦU@XRHkc;- tV4+ o0,lu2lڗj (%Et2RPs:ӒPKܖ}]VBռ`ڕ#֓Y { @q~!i,ڦ@ZZlIZXk)ͪF9@Q$4ϫG,j7@{ ObS]'1oîË ,]Y+W7R/a^Ƶc/L)'kMj(9ɴfZ' {6u\.JjmU8]Vi |ߪk\ c|сS*U GzI<CRmӛ-,^'S)/{Z-E7vI#i+/gA/{ٳӰS],bć;{zpm,oi% EXJ5_I<)2"s^g\{uL)'Ųc3u S#ĻaY $ګLG*IKrV!>J[Q Ԧ 3^ $sfDʡMB%n&$H
_Ѥ\Ѥ
Ѥ ѤhB7ŹmՕ
m$ }} l&+(6/_H-] b"/XٿLvB 'X
m[ H 6ҋr
/Vwfw sڳHFӪNۤq!^Q$ K˖cn~T|ԑVDbF//i
dSg h\>˗M-yNrDa'|J!T,E$i% )ȩΉx =4Pt[P.adÂK ;rI/c!T1%rI.Y% z`]M8[Gtgn|'dګ7۪~yx~Ʀ7Ź-d,Bo.Dg!Rq/%Y [c?H #g_Z룈ČA}}A?H@=HෂJ"!Q3W}$T4j"U,h"<, D,a HK M^y$CGH $^VpaFH"R)ދ'RA^P $ ѶzHf:"}滀ѲE"ߓDkn%Q$fHdX{(!H#! ]o+?ǣ ֫t͏&>c
.2smz1[,4]+/J"~,Y%$N}4p?exΡ w0ٖjAiEQEBU;@Mۣoy۵yfVnԟ1ʆ z*1_bTP̱CA;t u@JǕi4Bjj|$K*
&1TFX (XjTh]Xz.&W;r ?jC1 +ִKEׅG C]I< Ge+"^s3y YY~H%ÊӊF D6#2:Sq70`Md:`f2 *<;`Nfg ]m~<ʋd 2?Vr!V"("RÓBt@M *xXi O5}˽]:|0Zʻ1'ׄUUÖ:?$?g S4uXP wք Z@,ѵ,: v FdXq'\kT6I\^K[n߽}%N54mZAJ5Hy#^-w)'a e=}*-fh3:d*,%P{:upǜSEdt=s 4d*ˎױC{ &S*7A' A
w|vˏ`ZPl>pg/]7mM 9
9o<*hf~WނF=qV6"C: /Q̀䳕a->KlLi25poxkυ]80V
5C=5n+usmz~84=$1lM Nz9["voj+߽>KM }[Jiټ ޠr~ Co#xD/P㺖 Y.IcwsYt);ar~(
Ľ
0w 3s[uق \w;+g)PpM F,ʸfVp@i*\k)lݍ=/7ÆION.VPd\ir1t~Ě/_B)&ڌ>hk^Ƨ
KۂJ?N;$< (_DL `B]6R-K}_W! 6 < 4[j?`6LI[BvHpH}[˅Q>mV von
SRl<-s)mzJvWP:l p t%>z^FR\MY 7R7 2Qq/T؏~&yW[5S[=
n F_Ӫif}"5lس$h-52Q4gl LT;^4jQň7ZŵFj⒅=!Wy֯G >/_nU
b sZDg:SK ͫJ6vi_PAz D]j'+rNr {U!ucic| 箎3LYMIFzuWU[$C A
7swЬRFL\qBY0 x[}\E Ҥ{:8{lWuL cvzk̈c KSR> GfD?XН C]I,1e叛y=1yB@ pr.B*M쐈N"֡ϓ D88[7lV m<(-Z 6 YY:@Ha?o,|nֲks&m߿L>>pKu, ~ ;F&'{D
BrդsװHu& ײ-_&r"14~ڜH3> p53 s 4/h_K~+y{O g4}?[Ep`Y\+"On cR 9ةw-U̐l . b1@d51m*>a0= : ~HoVV(Yvl<|\s'8HD}PzSLh>F yǐxr:ZJ!6o)MQYQ\͙I267GN.ڰH1^~ rՊc:SSMzv(\{1k!s`q-/{ W{
吘.Soeԋ "#: k#mPUGiY=02r}A1Dj昔d3/yy ɩF)4JQLh.+"TT4r;s)4/0yij9
s"f jԛ~mbT!6dBR'c]AH1 lx]@tD1m>>Ӏ=f䢥dj](+M'zcy))YB1)՜VzNn"z[ ľ2"AzѠ[
jX #}aqL_`mi$_
bLR
.q<ھשdΟu9z =w{Zn.OL%^A̛ab+ ri}"aLxik] 4npTERahDp ZΥ N ~IވӫW$-jTg<ǁgP7)"Gx ֵpJiΜT x%Kr7US >*T2u$\tB$ o ^s|) kZ`-v*F L1*B{&d riɋ0D%.VM(9 $ML'j>n@sWMS3G;;7?(| ̅0A @\*&Y=ȋm'_>q/RSd oƦX\BBoTVc1#-PS
r `L^M82MC@7ť˝TEguCMEq`fIy*CUS Xd O6`nnz 007cLD3ŃbH]E8*gHx`d $SǛ k*2O _XVw
CnHòh9<?mec)t9RYSmJ Ԣ,Xn3 qt,/ `fΊh +J5GAZw:&i cY*yAxS^/qrI6ѝ+lCgĈs:svPce%s}PB_>ʹ2 dnZrN$R]8
`* σQ$dz%27SvFޒmR8rNvo%o.ǷGȝ ?20K ^.l9XƧ^_)Ht>''DVA:mXuKvqe =QtM Af&H_w~17k[NUɆ$LIڢ 4@GWU3.Nϵ4DΞ?mS+T zVp(x{jc'& 0F}ŦX H4{ )*㑕b+ArV;Vt,o'cYjT1ko[4rvOW lrF)+6/]բT Dk9DGfzr}FCȖsoOABmHƴCQҪCj#9Z*KdW*YϽsg:M{ wlcnh ʼ@k6j$:&m"qU"]2hЈq) 6R*LtXJwq%9';##xK oF8y;YTַlC:TQ,Q; 7`̓ sݴn֜kխZ8S@ ka[&fh6
*2 amEF \L!Uk ?= "2j"HdM `{&m9U"叿'Qk<]*y
mrр.hmEqx_,*\:s8'R7
$.KZTyU]MsB C/_`z62%u% X VYz0k_ߪĀ2T\,řptl8o =$K^IhqÞ*xBxi>`扺N|3q 5Q}zr$uUk#k}ZaCKqu^- G_K]1GdQM=ۥ4#ֶ[W$Jt9Ãj&kLzc~+CU44_ &.s6\J.4cwD5nlA]Цj Y` N 0*FES4g*,u,uTmҝ6 #´qD."šTWF >BdSW*,"*l _d,Fnξ d(x0ho# fRDmV]x,UCktˑlb 9Eb"wH(
ijXO+͏(xҾ3^|õXC"5v%>{K*$#UVU-UV *QoWW18Kc.Z FE<o]ܷ_G6[%?~kHHAՔѬ %vXNb%U\HA_}L`ojz*(d1M')%d i-he $ Ī',š x+9N'Jup2j.c! %$1V'e ױΊN] c%ӖDyx-ս冮{UD&iR."+krﾉS)dJVbgtNֵFmw^mXRt٣2PUv)v]28qG j
KS] &7U^⠤y[2[O\W(F+PJtϵbzL
VʷMiՕ: 35=|F55d˶1ueF_Gu^ا;$trtZ "wvmu*57eJ\%_k,ْN]$䭸$uj]j%nԐoJw
٨1!2y.J83|SSE-Ew:Ty,;jMƩĹ"
Pt\W|-DkX5[A4~s
$ɼ LƋU P2wN\w)+鞡ӽE=s^LW∶`i,*
eIFƿ-yqkj-^AL* 3Ucg.R-iAWA㙔"TYf/M`Β59Up<Ȋj;|gml~tڤi_KeI4ڳ5 \^+,퍼[>gֺLEmn#N ĕlr J>яm.GG'?N.p岔*-De ~XMĭ`f}=$ULjq1ťTq^WWGFn=5ժ+V"lXkU+xKP\jR(mi2f)9]5[b*,^}p+bdɽ o]#JN^ ^ :~Q."N\wl]Z/X#z2jȱ$b|ІѰD}riQ245#dԍNj4| d`Ai6$bN=
յYN 1hNu}&i༒#djfeX>3*DpC:NzYdKCs6>M"SvVT q? q,>(WG* {[7 T'
Z*ZgjFnN E-ҷ<5b8Ymft^(2old֪ɉc}XUج:mMZ 64T1/vM1<&$}5ªr[וLϙ=63i8II\]*)$*|C6/&Kr꜖[s
ەWbbway٩M
:¯D4#%F:l;ɕ^Ҷ.V' Rg#FM0G;]2O=
+G(։䒫zGHszQmts.q5 =hȕ `F\ђ_ _v收)6}ɀ]7{NFsmij*}*Ò6zd'i0um`F- QFKN/)kg|?|nfj?{jJ%r)@ V6cB5U3_]i vTvӘVW9|8ۘ]UQ>-WjQjG#V drԪecGk+=
F5H:flU:Ē*'jjuD~e9M&%^yH6ꢣHU6=/ˑ_k`ITSz=ܴj[hbH__w a(O ɲ VP^HIC
b]gzHW<HU&u ui rH;h93RA sEFnD+G%~
=1 A kud=RDe-PU
WaIߵt(:_rV:)7bQ 1\رsZ)Yֽ=$/bYW\I
u>32BkPűKNm7[ְ芍b8dbA}r_dսnW^\ej]4$5 u K\˷zɨn=+'q{ _su4H{|3)>e}K8+F(i;K#VI_Ot(TwVḺKl&kkɊqz_[u֫IXLu!Nh՛īZ Iax.DS֩I+5*n>Y| 2cu
T*\_Y""Z"rXK $uɰZ/]4!4sUSmOZ驵84aFVu\
i| =^( ߳iֿLmEJ0c#rgӶ^fVNQ eVYb$.ϊe(jgARn\ 'ĵV9>ӼZqѥr낓[W)x^m*1AʥNDX xx;و9D`Vn]F ^T2wFD7kVWzuktm\KkdP-/jnPAl&F>65PT#ġoAǵ&EJ|% 9Š=A^.G
~(/g4{IϗTJJ+_ӐpXa. UeĚ 3_ȡҲ&.Tr۪)vn}bI
V\F=WKuSyUWL1wOm%-ܘo\䬒qMgd:Y7]3nb^9)mөCUF{ul W']'͌Z:t5T*hc$|-LC&nxKz$z}DQ.&
[r*m\W?EI'5}bjZꊊNI:utbYŞ=66N`"Q5
tQ[5Zǃ֩\8u5hO_ /5cjUrѬt]d#۪/fH0%G\Rji<9Cqih}45R*]~J&1Au^eykIC/0V6TLxRZ5:ĸh1vE.PEH&_4cAnz
.^p4]b YkǸ'ϠS 76R
U??մ |ۏwݫgQhX˭#Y T {ƌUAGX4+9Fq)r1Y' )`m1t0 W'#fZC{5QiѷibSp1LtgZ$cT-
> j
6q(2*V|@AyN5˫t:U]Wb۳f<%{Bm
]_iΩ/XtHQ}_xllt`Ʒ"g;=Lq[*3#﹪vPrz:z/"IwvjviQ^yVVbS\)|ӪV,ipjhݺF_CKP4zF͘b0AͪP6cs)bx}:]kMSE{<
a-=
m]2g
PqD`Ǵlr@Cz*5jo5U~BhVЍVMѫda:@h!Y4.Ε[ق5i8zRlXlܰ!tMZwrdoa=D g*y91EկcceJ/w|)hsʵe}u,V+8_ec'ڀ
,GzնM^qt6Q5Oư-݃~gt2*5&>/ ot a rGĉr _r}u|w8AuPn$'\bqq]^W?t;2 _g!+ ; "ݿXcԁHth "u5Qyu ˋqZlRҕ ['G
y&s$셝(qKِS&Q/
|A\:9dRg_\/l5PaV[nm膒|:6~fA;#k+ZNWDx Jb&N늮?DbNYii4ub@hj#U);wKZxx>!nل6>yFo3%.H=1}t]lʱ7EWsJ!9yZW0Z ,xsşce3 aTSDfTbIv![|7n
Xل5D(([~WNbK K *hxM-ftK4iN'oXN$v@ grs!c* N|9
*ƣh'·:>&,OڥdiJuھ}he<4DΗw{RKx:ͳP/( JD:9uΚӋRN\JU oBX;=B-E: BUd9t*QJ%jJű,C[
u>C'xQ? :T6
Q qYm P#isD32
oV+L^
I4t^ c#24*mJu*ꪳ]ACGRn\DYTNڑ(FT Tic*U ⣝$DuCJ3PZ
Q5MtBR|oH@"TLݹ6sUJ'XsJ"mWdž_'&ʍ5^a
*oe7?zVue0d=̈!et
[2bcxYQ0A5Kγq`̤ t x3g@?^fmt'#N獺hbJZ z~K*|YIRA>6;u"[URK:=sGaYoLKT0쀑H},㸄TiC
ޕTE| %nPE2^, lqF$;f@%HŨUC/S;mFU,{+S _6J!x֞
Oub$KoEu:n֫Ng zSJ-a EzOio5&6]ȉZ
PqVN6/7`vPQ1ںZM5 '.6: հSY l.E͘qU/f;l8Fx-l&,ԶjJ\Z*:.5B1SxidZEv&AAF: jnj= lHh,t8gYK9>K`qHtz&sfluf5/4dg b-R6ڎBۆtQZMK. "aTw91-ʊ"gu5;鼫5q:r ֞O>%LRi U.Tj.u xwC%63$@^ձN0.
'xFEe 9*[JDt@20eHx]2v%6IEunlߩ*vfygM%%L#bQȇeR֪䲡4 StϴkM^|UNO Ȩ8 ً5zCh[=f7SknnM1Ce;d$x}gO ?ۙF+YEwm]8ڣg26dO@S.xiky^;z>o][2ڛ`2\7| ȬWm\ݒl45ST,H)5 )v5q%\A V4ݥV QQ=%.9Qk)MDUcK/uۖzfyp;: 0 v$V d5=ȀRld/c:߸I&D -%VW4"E( zWMS4JA'mӰ"jE ky<%+?V :r ݾ
j}wd-j*!f)#5XR n4*DJ,OT #46ޫSM;<%'ЩOFl˵>D=]756J m #3364KXb3 %QQKVIE9 ٺ8ht\
l<(*m8
M%ft
MU -f#YuGvjmbT "g&4i \kjܩDžh5L4;Aʼn;WifZ2]ՖN%HTڴFRXQNbhs<: +Cfh
i%1i1ꭦD%贆BwbYH Z# h()BDG
9ګagm"("n h"y>oiQG-]n͌FU?oiilm}K
kAb\(d&ߒ ]s!wTm#"#(ON|Ӕ%ȱQˆԢ;AJVrK#DZ$ED֫"fҫb%SPr QIZn2T^`
NҔ"Jɞ70FWx4d6"!6N=i=ē8AJlݚo c9@[3"%I5O[-X1&śj9g)u m.}.ri-+TxUs'{Zw/91E5\mf1 kR~äv`yvCb#h̷ (9Z\Ѻ r2ʰo4Ǝ ɑrPJ
K'b3rq VL&(JkDw-+cȮ)[Q/Xb(qb$UEMk
]4}@[1DT!utӱǘRZ\ZLX.1-Ʋ^(ͿRt5KUMQ]3hSd2'7XdNдr䩿$R%%쩉RF:הpY_ Rr'U,
u1e4&9&3'U2E0M;#ˡ]);i6(hyQ:VrZ)T?) 5*N%w[\M +#Ŕ[2
ʧMQ3P\>*e|!}>źO4{:`g߭}O}ز
Ip=\ܓ
r3]t:cxC/@w=`)u -u'SZ?[~9m6}):; ɿ]9;C>I"_^\NbkK @v7) yMUmf3mNqHɽMmݠӸ]j8r&{356/oԛj mBВ.u:T҈*5Y ڤsf\AKp\Otm[VxzU]S3QyY ӌFOۡ7~ۚ$6[qw _"UlLMV?_vMe"1Q[Yx9(ӱkͷʱŕڐ #fZTd6SrK"\)PeFvkNCF ~&9rD4Pٺo S) O2ՐJ*,f'/ԕ*~y#y&O EE
0A
+MعdHהu
<6|Yvj 1ϕSEc713v"sӲMkdʠ!V)/reqlgEld%ӉNb+e+PJնAͤ6_} f&SCD>i:
g4k 7pk|PdѲ˘X.[*e5MF:
SPb="7VpԇI8jm(7ƆbbKZʆZp\^{1d\ى^yys(WUvظˎYʤu^&cFBW
FXaEpIy]9QlQˀFؚ`NJjʑR
Zak=49\."7FfmMsnRVL04bg&Gv ]u3UMh4ЭN
6)$f|66M^3c)3zk隺Ͳjl)Niɗe۱
i˼~=9Nd-PcWny#T| ccvsB]1
I>4:\t-&b#LQme$IB{ Z ̰8Ϯ:S>HMAg*8jOM|AZ]fF5tJB:)SLE# ;6{)-8pGMt[X烞U qb3t! HT^dJW 981?'3|;m.pF}`ܑ #
Ѫ<~r$kΔ1A^UutQ א혘rO9JłJf^S^SZ ;jNvQÙKքZ9ኊi$ Š+&Ŕ[^A.J 5mͷ4t$UȴsQc3*O dn(j cu #?t\!aХ+˕T-d&ςa nrcxIgɘn("ۘAXMS_v[r͌ $lǑ4aK_4w"g1. ǎĸZ
Qv:r-!GR4d&R6Mlj'][s}hge"{8%7Vp|c>~ _},a 6Dע/*3;,Z?[WXG#9[մ[ Pu[Â˩ 9JN[_mSgy Hg9ED,znΊe|
_:qC)H7 iWtwcrhUކ~.InfHB9xOʾEY:땙ɪɎKTR
(DLUn9r i815j:JOtΌi֭jmpλj}Y~2{tEE%;ԕm/G
ɞorg e6lզ?749/or@n^`rTWvhsI#$JW-dvHw}J +hMNZCu+Ν,jr'eQ W50F2c 4@nsD pdyџy4t[1J P+6la R ښhUؐ9ds6sk ˻sJ
j_(yqn8"-\KzݩAy՟Z>KQ'.H#\-,96gϣrN?Щ.{'e@/{IKCkěCVU&MJ][
dFɛhd%SE^ &|bo+jɺ=
M7Ĕrx%2XrS5%jCjFltۛ#2^vMکk|_˵Hrc%?EԼ T>EImE1zgtzӔ҈/WծwTpI.TAW+iT"U eLR \N`>'E鋦H j7sy[pˑ#'!9y)4")_ Xv UZo?[jJ
VH&#yzzVϾȋC6ʉvՁoi
vYՙ: f{:ʍ2 y-8@iɌhl%2jȭOc+J,r]2ső:c }tEb#k:jаGaG
AyJsM4R'{t#'[!BuOQ 5ZИ%^ M%a[pёTͮei^!U+/73i)iVbЉ&,KzvǙBQG{쿨 նdGU[΄2T e֨Կf/ѺvX*q=]%+<2sV 1ILL+L)82*}\e~,ٓ`ѹƈcË+ZB ٪M`}[İ9BH l/2sXб? zP7{^R Y5*92!/!țd
U#&gIUcRrB]YfvPa"$T=T*NZh@zuNr ddy%=X Ti&'%&DK4bn1 \e[ĉs F͝VԆo f=SL".ˉf٥Yq9nSt!tqĞgsX9* m[QeK]kKbcS[MQkH-[R˭١\
ھ-b˿δe,ІY92J9dߔ_d \FkH9Gub',o1Oϵӎlۧ&tlG!tjtb9ąN2'juUlq Wv7zV-ě(Jaap&|6ۄMnPZ"˭/#jYVϰ~QM ]ge."WaIUN qV<,j
fy1Z6 9+;Qr{ 0'ֵ+$՜86hKİeH0+F:$H E߂q~"֨ ,m4) 4HU
đSَ =R` j?aCJ5a/k \׆\n;a=ȖP",)*QS%n &.VyOPh Vayk%r Ua[SiyP gYղ%u4Gi$v9 %
舮o5JɑeGZMUpfM[# zȡh ELAцB
^(.Hu-]YîW+H;NykhZ<'-9RQ(Vc9~sjՄe\
0SiO iCQϡ) %hB
j %8&LL$8A',t'یV&}хz\KעgӱQdƗŗ "+]wR"WI3&~-
\~ ā\;t@h:O 2n.'_-*1{晵h!hLH*JUM1;fRR(ZV̌K̑vA֧XM6R`/#+!)Vjl),iN-_}eʉ[G#]5 nW^Zb[rcN|5M)y̤iHR:afH>{]+NgaN*L%~>
U T\ 䦯]OqkOg{b"lձ: bԈNUQ ˜8FБa,l{Kۦ,=%|{r|KfLPØ\Wuwk Ri>M
&MWL
NJ)$R
ZłKbSS|=YޅX$][ E[UWD0C_.f./7Ŧ$4Ŕ1ZXsD*XAѯ(8r@VxVq-)9S2w)*O9D
QXjYpduZ~z T1TCF5YDPJL Gj⌔'ΔTѡ]k~X ,bBeG|WJ]3# 3@ JPqkG f/"0Ŏ{cz;]^ICCY}ٯ-#e`GKMN9XTe`I$\>ʴY2 +IU°) M1
<j/,-:|A m>dV,iJ,wV-VC tas\º Yp5!cUl!22* QQn9vM ti&F=缹L];u}] L s ǾWbwswr x";#3{=A Sw{ԹΝA=x<Ʀm6e+&zU'4evTi:V2i2?ǤiU&m?i i֦8uvc۽{M7
/2`|/ L,krrI~y4|hu`p6÷=\0@ 6 0'wG m1|b4s o4Ǘaσ70X};Ɵ5?41}o;Xe2at`hG1{p%Á L 5XxhO' _(/2%V/d6g_I_ͭG[ZJPW"ƆW _> 0<+&wc
U
pWCxw}2Rh]J)P v:5iI oM@mfZR
" h9ߢ5ҤP2RUk@ 5s+@[ߺts=/tzfj H?&ᝌ1+J7u.MIUIoգ>:蓃gFqt`+s$!ެ"J+FwiK/r(WW _k8 FOa1жq@z?=ZR:|TK Ya G> p 88IsiÁO)up&?81P!C?Ͽ '㽓# qA>E M$Byk {-/MJ (/D9q,L1U D:<|q plH't9 %bׯ54iIE &8m9g( g+.߄> |?8ώ.p .B w? 81{4H'au{K{.|d(Q«&%Nx-= ,\<;ᅣ/ VK_ ߹l*J`<[q1cË ѫ_Bs>ap~NG8i "1O/e &DEd6r=. / 8 wȣX(Р6k0
O'gg+|BW`pcFPTK{)K=
!6ncь
7d scHY7EiFlfB2d6Z X
C
6t ΄tōt <y&+8&am}`u&ц*=gp^{?`;+ <# <6!{3xrt7ѝ n1ϝCO' +s{oH5%4J J,J} + ~g9̯QC34jw1_O 'SEE""b|s1-}Ž qc1ni_!CF f< , " G_0Qx`㣟 #%01͟
~xxxx ~1.RY`p`,3ƲSLV "2~ V a}?p p/puww n;³W9x wV +(&Xw"ww#wk>^9bӌ3(ggPb WFW?5jsgQE_'<< <<8R`H!Yt<Hg "cPGnA{x hW7]\/:۸c0sh=
;8hf
?0=h77asxC.- 9n\#v߽y|` `_`? s 8$a3dQl X a
8(p ߨa_` fQ7D{ ݑn=+مQ+cxh:;
yYXy}.q-Ś;ށ05o oL887S <\^ ~O1Z x;pkZ.`m` pl q Z(5Q>k]ɻ^"BYx'~
mku|6?:{pgkWoMݐ7
!-g9z ckW#_8`J+P&@٬8x2r%+/WLV ?Xa?D V g ~? c 7=|$O;~"F
^+!`ı "||qe;-r_nONHH6HV1"Lnlo }I_KƂu ,PƘ4,0#
xwa@ CGfMol0[ [cEQ6;GYmܶ66f)6D(
Fx[VXLo3<rKȝ-!rk+֭!088<Y5n[[@~m8f_o9PA.L:@N̞Yu!׆_:a| 5x"캈g]!inF-`
nSE8
Ўz
Q&<6G D
gsM7f8KzGjo5|}pạ Ĝo^0Z"bX,~
x =0Ly0 i 0Yb+}
<_A b
;c3Fcc~1>h]Q'8 N³y_8 <{ a EG|q(PnP w>n_PE |o3ދ X7 πxp' C;ux
Rp2~ )x~
~NNg\TzMh`-
ow࿇w^ЯL ~Ȋ!7 ,!dуCB&?? w?t wc};6
&X__G|7 XW߄woF 7#!#7B#dB훱ྃ2n Gۻu}5pp9z)e/ x"<.;L\r*A^e܁o܁܉=7Q@?eS!ac/S:6ha0S`n(Vb~cf£ǀ36a ;O O*#g-Wss`;˞^Ӟ~0lCy^i?$xs~
<
s_a.΄gY<_SxI$$X @>o=<8 ~ o?<4.Bz++[^2hE)/&-Xe9?D`3' =];ہې5wfL M|f&`!~ \X&#~Ya V?!w>܇!C({;~>pp;pD">}3oF8MBFў)ǚ_Sī^0 ^>q
ëkވo{oނS{&Ȅ[ގ4Zyx;mTo*9e6;PNl* ʪ>9 T ?߇@vd-p! oĻ 1>܄5MX? 6Fg,0 ~Ɯr{-c\-2r
kFk}``k`K &&gNn¸v)_ lx7DbN[b#pzr<
]6tnKa<+6+s@n,Zm-46Hk@ ':q-p
p5PHA|Wan7B"܍Ӏ@]4 ;ߘйt} C"
E7 #Tƛ͐wK`+`k`|c[Ŀ-o
p` CcXm۶X nuX
| 8m$ENXk
>' vvzt{OSlYY|x+c ll lxv`8 x~2OA"2ƀ["_ǭfݚ a+`Kp[T K`SL_hn Zźz(63 `T+|"yv
0(+LG@y* 3 Ġ~q %ѱ 8D_::
=<}X.m±X tll4mV`26c|89%0lg;!H O >A cO xF1 }
491qDp= ߣX/h `>7' Db|? cKXr<ƒ1>:+x.D$9ON vFE3?}/ >g D xcřx~68p>pcGx .Az.E~y
{-~ :u(kQנ쿎z
5P?_|^i>ãڀMj $ЂHx" ҫ(MDG .J Xx _/ו|]sڜϙsf1X+),]L}eI&2G^m+_LVV%&®dvX!_I 5x}5BCHD}$8EտQxQ_N:Q:S 5 {K?~J DUHD} W?i>M %HhDy%>Y}pџu{ `ke2.-I{2m=mY cwyKIkwiG=E H{o?rom=h6F+{KL`k?B;pV'McC4@}ģ "{Žq֖udPdV0r?00`V!xϯCY^s/q3=_E~YwfZ7Y((3;^Ҿr"m#{d?h$ oi;>#m:yRfeQgu4\s9LlYn8XL &i<&.0 !BP/CǫDo..̨ Df$FESH)/MԛhNҿYT;9+o+oޟ͜똯߫6_ }{1sVڿ{/v%IFOǫxэ]YkIߋH2S9Q&Ih|g4|V9xRFcR 5ZŠ.iD4BiMh^cғPKK#GV @?$֯#t]b%;~֓F]2Et "QbĢ6jr^hFM5QզϵO"hmugNVۈb uHL}4@C$qLNcS&ɨķ
:!QID]cQ2PQJZe#h aq^'v*ocфCCh椵Zg5/3&͉S3ьI%+W9f2(R(P\sV+` "?z̭ - ͥT khA[f+!-PʅR^)璤)vњ!ǃZCy!reP1v,$2
O8"iCA,PG+o%1R噃e (DrjJ M 9J e?G\x-HD9 (&JR(e8p @E)B|jHaBA G!0Wg"<1|@Z eeM$ňe1bD34ъ5OQx0̕@f1b}%Śn&k-^ Y<1zhy)QGOz=ГkF/"0h__gt]g"}x;ӂ^`l;j% BZ(H(R<|Qa(O;gO:q8sQ\[uGQ)(
䇣w<TvTAUM:S^Jz5FN>zٞ5iִgY۞e k g{;]Y=Y{{k ]}N{>
Fo
YS༻raS<OWfF$>ypù owqyX}jZl qaݫzx$>< xNs}kH$&~6v4#l7{ěHrmX۲?i3c gdȭH I˯/ kя?Q:ڠ5ZVXS3Z
з|{D.⒋"ƹu.bo1^ 'Y2֊X!/ boH_LZB.Yx}Q{W{ʞ;UӺk(Ңn M}8:x I"A:9:j5P};w(((UhhhhOxx#yv#yn9js_'OO=3w yu ~gyQڃ 97)
W$~ᔭ_~\%W o~>e0F,3,RQQAT7"VQJz;S3o(wYuqՍa+sq%OW.QG{Ϊ7m7'~w/tڋy\ ߒe7[.KI[$y3Ա,Hזb e|Y<>,݇ 97-R,|tnw'%>[B%o۸V\g>#} 1Oq)s(5ugȗYJӾ̾L̠gM2ݽQ>uF>wJT/soB|C->J19G\c{-%F눣]5H*m9Sg%eV9R j&ik5mWҧgZ^W4Lzrc=m즽={eI?=,'>8Eh=Qb&/1|K{{ i~{DZ[geydLJ ɔD&;&`ݱSOl'h[F- Vzl)MCx2&e2Q[XeXʵїei9Y7N[XF,%~)R`9V`%cr
i + ;ckNۀXXHFmg;A?wb(.|˹j. !lj 3:QYQc>t&ə|H SSqx!L&(SP;c*> Εw9aC K/l{?8|C|sHs ؓ/p[e<ȫ>-?/ΖD3 Y`d~ǯ"7S/[Mk Us_fd|]!2e/臾ͤQf+i311@ w`'ߓ axwڐ'$>xC;q0MpE䍠HޣFpӼu}Oҏ loi 7;c rUbM0oY:(7d"LDI] ,ҰEFe(WrvwwX{2](F
)L9CNS4O9k֫kbo NGswLǎi}锽SLӮSg B/ YEfDki TynÞKo wo sߣ[:_SWdTq~VQø*>WpYjqq陜Rm-]bJqF1NNE#8u_ bP Q h0IqP(Ds^ZE ģ>~i`n>/ Nvhvj.z1ӷmm+}K:2WW\>om"4*i)alz|5驔KT=koz~o so (GԯaRM*bJ5X ї$ғoDF
rptn*HT +
8-ޗs+ϵ*q?8O*31X1~ q{Hߍ R~;@>т){> > J~(Jj{JΤ +EJ1BBRB۩Pt)ơQyY)|#L[yF0c=b
竵0[)2x*˱k/
~+q2b-1Ud)1_w t-ӊ0u
ӏBj{Ͻ'ׂF* I[X˹v7`L3] EP,8bnb,Y0km!ꜗnquίjB.YJʿ"y//(s e}\ڕ(\ pޯngEߢKܻR4@ٻ98&=)IiǙGpԯ1 whǙǙǘǘGGG<* Jwqtv& A\*}dONkhptsX?/
:u~zW)sX//jյK\{Dη,]pqryFn;!.`XvAÄ]
V$K*^h#EH^13\vdl+(Az;~ꙡ]Ji2k[Z? #=2JY>n:~acU(ˌ+l*ˬ*z93< ?GҔRO*^'CY|Nha/LOqot/2r8v٬ "?q0^=jlse-otry7= UU3X5:
xr؟mB^eR^٦y ;4bN泛;~Lf?yyiLLx~c;y(Q̸?;^xO ?ȇ
| {|WV"OoZdZd< <> gIW7o^1 'cݱƹkZƻkj Oejc:c EF%%Es({KHʍ$#rfBbNdK0Wo̽x栒H$!yIh"cQFDFʠVP#od[ jMj&=8A](uDWND\AD8Q8Ղ AZ $?r+J}jjv
Qۉpqls/y|TP'10&Dk{x)NR¡ΫC.{-{)0)KqzlF}FqGj/;>Qy1q#JDx>/`PӉjk{3QDD|kF6' s1/`36qt!}CW`fwZͮt
kZ:zA DQ(Y{zo(ItBZ
16ݭ8/N$}֒a[[fY3c^n҂QQ!)|56#moiVl&ο5rV1|KLRnwۍ]!&r+VοPӿW0Yi$zc- ! /BcxPR46ҶwvV9&;AAAz|VVaI_?8Q ss!i &Cev{ 0iGq ?r~389\eΕ[,-2E%7粈 SoX/ /9 ]Y
:upϔe>Y)frǕ -)q0)߯Y
U1r/D"QH.ū r~`˜i<)t|9Ogi
?2zO2 |Γc\csϽy~3~{dwϏy͏'T9d9@rsU';gv}O B8ǟ8?EDG"{h 丏sU>;}o~$9D?$$9HDQd|G=R~q#4y=|2 9^Y~(#.ޓ Q.w]Iv>߱oZW[3˟>DdD?H?FcD(>0H?tzf9ӉT:J'D<"IH"zȞ'7 wJ+tϖ7윕oVQ[HĔDLY̭tfevOEV) OܫoT'2I F
`Dx|`T2ֈ»Z8yQIfq\E|lz_QKڙI{3iw,:S1"cd1@veUϠ^ hkmviᤇApY-BN$~ 19F{Gi ^=Pc\u"S~2N {Fd^i83+I|jDJT8OĠkᤇK4VG0zWۈ[̄_ט qI '-\~g&yg WpOe^)tF=$~
Ϡ#<#gtNވs5ҪW2N<.ݘ 8"$C0ן}i/ݾߟ zZ2m%f2LlqF,5
39N9Nt?D!Zzjb f=Iқqn!foIf܆1NA2 dyCyey|TZh<̘^k} Oj%K"ZLKmơ. -u-ִZ3gv2Kft$--Bk}d23ZٌWӉ4ffM| S?U["]k {p_Cd:m ) 2jc̞b$cL2@A,FsSw!N2d+f8?LSY>e~mVfEYTSHYmƊ켏d$c7D !C<LJX#F'{Yv{ ~b]!7p
Wpzvy=O%w^7pScO8Z^pF,[E,oU1ax#卖<7o< @ي nƃhhAÔiIG奵~TVꈡL j4#7J V&iDiJ7IwTAR;XPWK&=Y*!E |(JR"꾳3x 3@{oey!Q-\Eo%qw-G_AoaN_fHos%Sh{*3k*SNDLZ82k|q!ŗԙA(ok@o͈0cqψOćZ2y2 C,=ч15۟{#C*yy t[$
*Rê%uRjűk%5T Wӌqrۆc1W%?\T{R(aV hB$j6xH*YRފRV*}Vx87^.{am/7%&}Qmg|47ruZH/K $&2j$iڡ o'd V[yQF?y(uKBĻ-di
&x(߂FKjEh>W#
y)ADPW 'o hU~e%oYq2̪#C-C:mfE`*PE"[8\46KV~2Acl7K,4RkfdqueyF>{Q^o7B# OE>o}(h_#fo7+91JڟRo gؒbq=kL7V\Ҙ/یr''rX$7
cB_UZOSĮ$xVIeB|#5<%3Wx`E=m{Ig<Ч Չ6;覅W~ Myh$4R8h? }vHIj(L .:lnZHa.3*6H s>Knx\"{_=K,Zl| ,ffq4Kؖb5CZ17t a40x
gɳd:#,Mgf{
!?$VzK1Γ&{Q E C iaXH! J7֛|Q.r_#=2³B,%g m> d4&`**yg
pw3%Pƌ(̨`)1Th
2)g~+a̶̲(`mgVF! qF' uks ycyBZ?㤴G',ySnjϘΆ`U(S,@.eى ZsY65
ik\/<#qZ~:!
Q 1>y}*i?7z_]\c1(\.ͥ qz`p ; /U 3a 0Ab1\Xx gO0/O2?O3K̃K̇̋c؏B+h\Aݙ̉/;; H #=1a;IQMchk m{<-_cyJV0~`nuI5W2/ |AT=s\7-
[6[ Hwe~+o,pCOɏ蝏R a(%BL{L\8 %!vi/"ʣfÍ켧]Ĩj!ua=bOLm}b\X'xb_1X2&PoHd :rMe7M{ oG^~[~
;3VO1F͐ΣPh?-n *yox# {mQ2»CnUҋ~wvhg^v
2u")Foe-߉UF$Q:Ȩ]/[d3#l^6D$wBlmպ--.KFWM_](rUܔ0BuKJP8mV JoVS־-g cvRon|iƻ_nŻTzOyr;̓)l-BBPbOYA"ѨֶJ1V kC R%0kj[JMkD[%U'o$G=8 oI?kVKO{Z*/^ uNHGh(]c:BCڏQ4.CHq({:{6V:mӶR~
p_Op Н֏7*l,-+U jٽё(6Z틫
Zz|+T=z$/>\ `Y{ ff ` R>& - {p _/ ̴ > ? " d d D | ? " d d D g Z " D M
A X n ? " d d @ @@ `` P R D
` p > Z M A : : > M A : 4 4 V (
T _ @ @ @ @ 1g
T Click to edit Master title style !
! 4
N ,a @ @ @ @ c1B
R Click to edit Master text styles
Second level
Third level
Fourth level
Fifth level !
S
N n @ @ @ @ CI
\ * - DDD
N q @ @ @ @ C"I
^ * - DDD
N 4| @ @ @ @ C%1I
^ * - DDD
H
0 nF! ? 33 8 0 _ _ _ P P T 1 0 . N D e f a u l t D e s i g n > 0 w= o= ! = (
x
c $ ` < 4p
0 5
t What the Research Is 2 D p
0 ]
The aim of my research is to use machine learning techniques to detect patterns within logical theorems and use them to guide automated theorem provers. 2 . D
0 h ]
t The Intended Outcome 2 D
0 !'
N The primary aim is to extend the range of theorems that can be proved automatically in reasonable time.
A secondary aim is to develop an understanding of structure within theorems and how this may be exploited in theorem proving heuristics. 2 D
0 4× (] *
x The Stage the Work is at 2 D
0 \͗ 7* 4
x I n i n i t i a l e x p e r i m e n t s I v e r u n t h e o r e m p r o v e r f o r a s h o r t t i m e , c o l l e c t e d d a t a , t h e n r u n t o c o m p l e t i o n . I a p p l i e d m a c h i n e l e a r n i n g t o g e n e r a t e a c l a s s i f i e r t o p r e d i c t w h e t h e r o r n o t a t h e o r e m w i l l b e p r o v e d w i t h o u t n e e d i n g t o r u n t h e p r o o f p r o c e s s t o c o m p l e t i o n . R e s u l t s a r e p r o m i s i n g b u t i n c o n c l u s i v e . I n o w p l a n t o e x t e n d t h e w o r k t o l e a r n i n g h e u r i s t i c s e l e c t i o n f r o m t h e o r e m d a t a . 2 . ( R D
0 ]e
m
The Challenge 2
D
0 ` c
Using computers to search for logical proofs of theorems has many applications ranging from pure maths to hardware and software verification. But the power of computer theorem provers falls well short of the initial promise of early work. The main challenge is the enormous size of the search space containing the proof being looked for. Much progress in search heuristics has been made but different heuristics work better with different theorems and determining which heuristic to pick for a new theorem is not straight forward. 2 . [ D
0 ( 4]F6
# Preliminary Results and Conclusions $ 2 $ # D
0 l 2
! Logic Systems and Theorem Provers " 2 " " D
0
2
+ g In logic there is a trade off between expressive power in stating theorems and the decidability of the proof process.
The simplest logic is propositional logic where theorems are boolean expressions and the proof process is described as satisfiability or SAT. SAT is decidable but propositional logic is too simple to express many mathematical ideas and problems. Even at this level, for general expressions SAT is NP-complete and there is unlikely to be a polynomial time algorithm to solve it.
First order logic adds existential and universal quantifiers and allows functions so is significantly more powerful than propositional logic. It is semi-decidable. Most automatic theorem provers work in first order logic.
Beyond first order logic, higher order logics are widely used and are particularly useful for expressing complex hardware and software verification conditions but cannot generally be solved automatically. Instead proof assistants are used which require expert human intervention in the process.
Much work is being done on combining automated first order logic provers with higher order logic proof assistants. h 2 h | 3 * D
0 R29
* Automatic Theorem Proving and the E-prover + 2 + " $ D
0 H, 2%
h
A b r e a k t h r o u g h i n t h e a u t o m a t i o n o f t h e o r e m p r o v i n g i n f i r s t o r d e r l o g i c w a s t h e p u b l i c a t i o n b y R o b i n s o n i n 1 9 6 5 o f t h e m e t h o d o f r e s o l u t i o n . I n s i m p l e t e r m s , t h e p r o o f a p p r o a c h t o a t h e o r e m i s a s f o l l o w s . I f a t h e o r e m i s t o b e t r u e i n a l l c i r c u m s t a n c e s , t h e n t h e n e g a t i o n o f t h e t h e o r e m m u s t b e i m p o s s i b l e ( n e v e r t r u e ) . T h e n e g a t e d t h e o r e m i s e x p r e s s e d a s a s e t o f l o g i c a l c l a u s e s a l l o f w h i c h m u s t b e t r u e f o r t h e w h o l e e x p r e s s i o n t o b e t r u e . A s e t o f r u l e s , o r l o g i c a l c a l c u l u s , i s u s e d t o g e n e r a t e n e w c l a u s e s i m p l i e d b y t h e e x i s t i n g c l a u s e s . I f , e v e n t u a l l y , a n e m p t y c l a u s e w h i c h m u s t a l w a y s b e f a l s e i s g e n e r a t e d t h e n t h e n e g a t i o n o f t h e t h e o r e m i s f a l s e a n d t h e t h e o r e m i s t r u e .
R e s o l u t i o n i s a s i m p l e m e a n s o f g e n e r a t i n g n e w c l a u s e s t h a t R o b i n s o n s h o w e d t o b e a c o m p l e t e a n d s o u n d b a s i s f o r a u t o m a t e d t h e o r e m p r o v i n g i n f i r s t o r d e r l o g i c . U n f o r t u n a t e l y t h e n u m b e r o f n e w c l a u s e s g e n e r a t e d c a n r a p i d l y g r o w t o a n e n o r m o u s s i z e a n d t h i s i s p a r t i c u l a r l y t r u e w h e r e t h e c l a u s e s a r e e n c o d i n g e q u a l i t y a s a l o g i c a l c o n c e p t .
T h e a n s w e r i s t o t r e a t e q u a l i t y a s a s p e c i a l c a s e , i m p o s e o r d e r o n t h e p a r t s o f t h e l o g i c a l e x p r e s s i o n ( l i t e r a l s a n d t e r m s ) , u s e a s e t o f r u l e s r a t h e r t h a n j u s t r e s o l u t i o n a n d r e m o v e r e d u n d a n t c l a u s e s e f f i c i e n t l y a t a n e a r l y s t a g e .
A n e f f i c i e n t s o l v e r u s i n g s u c h a n a p p r o a c h i s E w r i t t e n m a i n l y b y S t e p h a n S c h u l z a t M u n i c h . T h i s i s t h e p r o v e r t h a t I h a v e b e e n w o r k i n g w i t h . z 2 z . T D H
0 1 &2'
A P r o o f i n R o b b i n s A l g e b r a A S u c c e s s f o r A u t o m a t e d T h e o r e m P r o v i n g ! F 2 F E D
0 T[ '2,
$ Despite becoming increasingly sophisticated and useful in a range of fields such as software verification and security protocols, automated theorem proving has not become a tool for mathematicians in the way that computer algebra packages have. A notable exception was the proof in 1996 by McCune of a conjecture by Robbins in Boolean algebra which had eluded human mathematicians for over sixty years.
Though the likes of Andrew Wiles are probably safe for the time being, the original aim of theorem proving, to do maths, has been given a fillip. % 2 % $ D
0 b -2.
T M a c h i n e L e a r n i n g S u p p o r t V e c t o r M a c h i n e s + 2 + * D m
0 $f -/28
k Machine learning involves using a computer to find a relationship between measurable features of a problem (eg temperature of a patient etc) and some outcome, typically a classification (the patient has measles or does not have measles). Rather than analytically model the relationship; instead, parameter values in a model are estimated by looking at historic data (the learning process). If this is done correctly, the same parameters can be used to classify previously unseen data.
In a support vector machine the numerical values are transformed to new values in a multi-dimensional space which may be of different dimension to the original feature set. In the new space the values can be partitioned in a linear fashion and classification is determined by which side of the partition a transformed point lies.
Following advice from Sean Holden, an expert in the field, I have so far used the program SVMlite to generate classifiers in the form of support vector machines. At the same time I have passed the data on to Sean Holden and Andrew Naish at the Cambridge Computer Lab who are able to apply more sophisticated methods. l 2 l Z l Q D
0 4r ):2;
~ Finding Features in Proof States ! 2 ! D
0 , g;2dB
I n t h e o r e m p r o v i n g a p r o o f s t a t e i s t h e c o l l e c t i o n o f l o g i c a l c l a u s e s , d i v i d e d i n t o p r o c e s s e d a n d u n p r o c e s s e d s e t s , t h a t p r o v i d e a s n a p s h o t o f t h e p r o o f p r o c e s s . T h e i n i t i a l p r o o f s t a t e g e n e r a l l y c o n s i s t s o f t h e n e g a t e d t h e o r e m t o b e p r o v e d t o g e t h e r w i t h t h e a s s o c i a t e d a x i o m s a l l o f w h i c h a r e i n a n u n p r o c e s s e d s t a t e . A s t h e s e a r c h f o r a p r o o f p r o g r e s s e s t h e n u m b e r o f c l a u s e s i n c r e a s e s a n d s o m e a r e m o v e d t o a p r o c e s s e d s e t . T h e p r o o f s t a t e a l s o c o n t a i n s i n f o r m a t i o n a s t o h o w t h e g e n e r a t e d c l a u s e s a r o s e .
T o a p p l y m a c h i n e l e a r n i n g t o t h e o r e m p r o v i n g r e q u i r e s a m e a n s o f m e a s u r i n g f e a t u r e s i n t h e p r o o f s t a t e , e i t h e r f o r t h e o r i g i n a l t h e o r e m a n d a x i o m s o r b y r u n n i n g t h e p r o v e r f o r a s h o r t w h i l e t o r e a c h a m o r e c o m p l e x p r o o f s t a t e . P o s s i b l e f e a t u r e s a r e c l a u s e r e l a t e d ( e g c l a u s e l e n g t h ) , o r i n v o l v e w h o l e s e t s o f c l a u s e s .
M y i n i t i a l r u n s u s e d 1 6 f e a t u r e s , t h e n u m b e r w a s i n c r e a s e d t o 6 0 i n l a t e r r u n s . 2 H ^ D
0 J3[
2 James Bridge supervised by Professor Larry Paulson 3 ( 2 3 2 D P
C ( A C U n i b i g '
0 CD2*E
n Acknowledgements 2 D
0 E2G
, I have received much guidance from my supervisor Larry Paulson and from Sean Holden. Andrew Naish has analysed the data I have generated using his own software and Stephan Schulz, the author of E has provided ideas and patiently answered my e-mails despite having a full-time job outside of academia. - 2 - . \ D
!
0 h 6C
P Working with approximately 1200 theorems in the SET classification of the TPTP library led to a classifier that was correct 70% of the time but the sample was skewed so the base line would be 57%. The tentative conclusion is that useful results may be obtained from machine learning but that more work is needed on feature selection and learning methods.
Rather than remain with classifying theorems into solvable or not, the new work will be applied to the more useful area of heuristic selection. 2 D H
0 nF! ? 33 8 0 _ _ _ P P T 1 0 . r 0 ' 6M 1 ( 4 J
b / 0 D A r i a l N e w R o m a n L L Oh +'0 hR ` h
$ 0 8 < Applying Machine Learning to an Automatic Theorem Prover James Bridge James Bridge 26 Microsoft Office PowerPoint @ py @ `@ 7 4 G (Q ( a& """ ))) UUU MMM BBB 999 | PP 3 f 3 33 f3 3 3 3 f 3f ff f f f 3 f ̙ 3 f f 3 3 3 f 3 3 3 3 33 333 f33 33 33 33 f3 3f3 ff3 f3 f3 f3 3 33 f3 3 ̙3 3 3 33 f3 3 3 3 33 f3 3 3 3 f 3 f f f f f f 3f 33f f3f 3f 3f 3f ff 3ff fff ff ff f 3f ff f ̙f f f 3f f f f f 3f f f 3 33 f 3 f 3f f3 f f 3 3 f ̙ ̙ 3̙ ff ̙ ̙ ̙ 3 f̙ 3 f 3 33 f3 3 3 3 f 3f ff f f f 3 f ̙ 3 f 3 f 3 f 3 33 f3 3 3 3 f 3f ff f f f 3 f ̙ 3 f 3 f ff ff f ff f f ! ___ www 18 4 a& A q ( q H ʦ """ ))) UUU MMM BBB 999 | PP 3 f 3 33 3f 3 3 3 f f3 ff f f f 3 f 3 f ̙ f 3 3 3 3 f 3 3 3 33 333 33f 33 33 33 3f 3f3 3ff 3f 3f 3f 3 33 3f 3 3 3 3 33 3f 3̙ 3 3 33 3f 3 3 3 f f 3 f f f f f f3 f33 f3f f3 f3 f3 ff ff3 fff ff ff f f3 ff f f f f f3 f̙ f f f f3 f f 3 33 f 3 f f3 3f f f 3 3 f 3 ff ̙ 3 f 3 f 3 33 3f 3 3 3 f f3 ff f f f ̙ ̙3 ̙f ̙ ̙ ̙ 3 f ̙ 3 f 3 f 3 33 3f 3 3 3 f f3 ff f f f 3 f 3 f ̙ 3 f ff ff f ff f f ! ___ www ݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻ ݻݻݻݻݻݻ ݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻ ݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻ ݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻ ݻ ݻݻݻݻݻݻ ݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻ ݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻ ݻ ݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻ ݻ ݻ ݻݻݻݻݻݻ ݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻ ݻݻݻݻݻݻ ݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻ ݻ ݻ ݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻ ݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻ ݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻݻ ݻݻݻݻݻݻݻݻݻݻݻݻݻݻ & " & , 2 $ /4@DeFY,-KG dS 0 A A @ 3 ʚ; ʚ; g 4 2 d 2 d d 0 p A% p P < 4 d d d d A10L 8 0 _ _ _ P P T 1 0
p p 6 Applying Machine Learning to Automatic Theorem Proving 7 7 B 6
dC 0 B B % dB (
x
c $ t < 4p
0 ( 5
{ The Nature of the Research 2 D p
0 ]
The aim of my research is to use machine learning techniques to detect patterns within logical theorems and use them to guide automated theorem provers. 2 . D
0 Э h ]
$ The Intended Outcome of the Research % 2 % $ D
0 !'
N The primary aim is to extend the range of theorems that can be proved automatically in reasonable time.
A secondary aim is to develop an understanding of structure within theorems and how this may be exploited in theorem proving heuristics. 2 D
0 H (] *
~ The Present Status of the Work 2 D
0 p 7* 4
x I n i n i t i a l e x p e r i m e n t s I v e r u n t h e o r e m p r o v e r f o r a s h o r t t i m e , c o l l e c t e d d a t a , t h e n r u n t o c o m p l e t i o n . I a p p l i e d m a c h i n e l e a r n i n g t o g e n e r a t e a c l a s s i f i e r t o p r e d i c t w h e t h e r o r n o t a t h e o r e m w i l l b e p r o v e d w i t h o u t n e e d i n g t o r u n t h e p r o o f p r o c e s s t o c o m p l e t i o n . R e s u l t s a r e p r o m i s i n g b u t i n c o n c l u s i v e . I n o w p l a n t o e x t e n d t h e w o r k t o l e a r n i n g h e u r i s t i c s e l e c t i o n f r o m t h e o r e m d a t a . 2 . ( R D
0 ]e
} The Challenge to be Addressed 2 D
0 t c
Using computers to search for logical proofs of theorems has many applications ranging from pure maths to hardware and software verification. But the power of computer theorem provers falls well short of the initial promise of early work. The main challenge is the enormous size of the search space containing the proof being looked for. Much progress in search heuristics has been made but different heuristics work better with different theorems and determining which heuristic to pick for a new theorem is not straight forward. 2 . [ D
0 < 4]F6
# Preliminary Results and Conclusions $ 2 $ # D
0 l 2
! Logic Systems and Theorem Provers " 2 " " D q
0
2
g In logic there is a trade off between expressive power in stating theorems and the decidability of the proof process.
The simplest logic is propositional logic where theorems are Boolean expressions and the proof process is described as satisfiability or SAT. SAT is decidable but propositional logic is too simple to express many mathematical ideas and problems. Even at this level, for general expressions SAT is NP-complete and there is unlikely to be a polynomial time algorithm to solve it.
First order logic adds existential and universal quantifiers and allows functions so is significantly more powerful than propositional logic. It is semi-decidable. Most automatic theorem provers work in first order logic.
Beyond first order logic, higher order logics are widely used and are particularly useful for expressing complex hardware and software verification conditions but cannot generally be solved automatically. Instead proof assistants are used which require expert human intervention in the process.
Much work is being done on combining automated first order logic provers with higher order logic proof assistants. h 2 h b * D
0 2s
* Automatic Theorem Proving and the E-prover + 2 + " $ D 2
0 + 2!
B A u t o m a t e d t h e o r e m p r o v i n g d o e s n o t r e p r o d u c e t h e c o m p l e x b u t r e l a t i v e l y s h o r t p r o o f s t h a t h u m a n m a t h e m a t i c i a n s p r o d u c e . I n s t e a d s i m p l e l o g i c r u l e s a r e a p p l i e d t o m a n y c l a u s e s u n t i l a c o n t r a d i c t i o n i s r e a c h e d . T h e o r e m s a r e p r o v e d b y d e m o n s t r a t i n g a c o n t r a d i c t i o n i f t h e n e g a t i o n o f t h e t h e o r e m i s a s s u m e d . O n e s u c h r u l e t h a t m a y b e a p p l i e d i s r e s o l u t i o n ( s h o w e d t o b e c o m p l e t e a n d s o u n d i n 1 9 6 5 b y R o b i n s o n ) . T h o u g h m o r e c o m p l i c a t e d r u l e s a r e n o w a p p l i e d , s u c h s o l v e r s a r e o f t e n d e s c r i b e d a s b e i n g r e s o l u t i o n b a s e d .
T h e p r o b l e m w i t h o n l y a p p l y i n g r e s o l u t i o n a s a r u l e i n a n a v e m a n n e r i s t h a t t h e n u m b e r o f n e w c l a u s e s g e n e r a t e d c a n r a p i d l y g r o w t o a n e n o r m o u s s i z e a n d t h i s i s p a r t i c u l a r l y t r u e w h e r e t h e c l a u s e s a r e e n c o d i n g e q u a l
! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9 : ; < = > ? @ A B C D E F G H I J K L M N O P Q R S T U V W X Y Z [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~
8 ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 7 9 : ; < = > ? @ A B C D E F G H I J K L M N O P Q R S T U V W X Y Z [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z | } ~ R o o t E n t r y dO ) 6 P i c t u r e s dS C u r r e n t U s e r D S u m m a r y I n f o r m a t i o n ( R P o w e r P o i n t D o c u m e n t ( þ D o c u m e n t S u m m a r y I n f o r m a t i o n 8 Ԗ 0Ԗ " D T i m e s N e w R o m a n L L Ԗ 0Ԗ @ . D
@ n ? " d d @ @@ `` & $ & , 2 $ /4@DeFY,-KG dS 0 A A @ 3 ʚ; ʚ; g 4 2 d 2 d d 0 V p A% p P < 4 d d d d A10L 8 0 _ _ _ P P T 1 0
p p 6 Applying Machine Learning to Automatic Theorem Proving 7 7 B 6
D 0 C xC % C (
x
c $ t < 4p
0 ( 5
{ The Nature of the Research 2 D p
0 ]
The aim of my research is to use machine learning techniques to detect patterns within logical theorems and use them to guide automated theorem provers. 2 . D
0 Э h ]
$ The Intended Outcome of the Research % 2 % $ D
0 !'
N The primary aim is to extend the range of theorems that can be proved automatically in reasonable time.
A secondary aim is to develop an understanding of structure within theorems and how this may be exploited in theorem proving heuristics. 2 D
0 H (] *
~ The Present Status of the Work 2 D
0 p 7* 4
x I n i n i t i a l e x p e r i m e n t s I v e r u n t h e o r e m p r o v e r f o r a s h o r t t i m e , c o l l e c t e d d a t a , t h e n r u n t o c o m p l e t i o n . I a p p l i e d m a c h i n e l e a r n i n g t o g e n e r a t e a c l a s s i f i e r t o p r e d i c t w h e t h e r o r n o t a t h e o r e m w i l l b e p r o v e d w i t h o u t n e e d i n g t o r u n t h e p r o o f p r o c e s s t o c o m p l e t i o n . R e s u l t s a r e p r o m i s i n g b u t i n c o n c l u s i v e . I n o w p l a n t o e x t e n d t h e w o r k t o l e a r n i n g h e u r i s t i c s e l e c t i o n f r o m t h e o r e m d a t a . 2 . ( R D
0 ]e
} The Challenge to be Addressed 2 D
0 t c
Using computers to search for logical proofs of theorems has many applications ranging from pure maths to hardware and software verification. But the power of computer theorem provers falls well short of the initial promise of early work. The main challenge is the enormous size of the search space containing the proof being looked for. Much progress in search heuristics has been made but different heuristics work better with different theorems and determining which heuristic to pick for a new theorem is not straight forward. 2 . [ D
0 < 4]F6
# Preliminary Results and Conclusions $ 2 $ # D
0 l 2
! Logic Systems and Theorem Provers " 2 " " D q
0
2
g In logic there is a trade off between expressive power in stating theorems and the decidability of the proof process.
The simplest logic is propositional logic where theorems are Boolean expressions and the proof process is described as satisfiability or SAT. SAT is decidable but propositional logic is too simple to express many mathematical ideas and problems. Even at this level, for general expressions SAT is NP-complete and there is unlikely to be a polynomial time algorithm to solve it.
First order logic adds existential and universal quantifiers and allows functions so is significantly more powerful than propositional logic. It is semi-decidable. Most automatic theorem provers work in first order logic.
Beyond first order logic, higher order logics are widely used and are particularly useful for expressing complex hardware and software verification conditions but cannot generally be solved automatically. Instead proof assistants are used which require expert human intervention in the process.
Much work is being done on combining automated first order logic provers with higher order logic proof assistants. h 2 h b * D
0 2s
* Automatic Theorem Proving and the E-prover + 2 + " $ D 2
0 + 2!
B A u t o m a t e d t h e o r e m p r o v i n g d o e s n o t r e p r o d u c e t h e c o m p l e x b u t r e l a t i v e l y s h o r t p r o o f s t h a t h u m a n m a t h e m a t i c i a n s p r o d u c e . I n s t e a d s i m p l e l o g i c r u l e s a r e a p p l i e d t o m a n y c l a u s e s u n t i l a c o n t r a d i c t i o n i s r e a c h e d . T h e o r e m s a r e p r o v e d b y d e m o n s t r a t i n g a c o n t r a d i c t i o n i f t h e n e g a t i o n o f t h e t h e o r e m i s a s s u m e d . O n e s u c h r u l e t h a t m a y b e a p p l i e d i s r e s o l u t i o n ( s h o w e d t o b e c o m p l e t e a n d s o u n d i n 1 9 6 5 b y R o b i n s o n ) . T h o u g h m o r e c o m p l i c a t e d r u l e s a r e n o w a p p l i e d , s u c h s o l v e r s a r e o f t e n d e s c r i b e d a s b e i n g r e s o l u t i o n b a s e d .
T h e p r o b l e m w i t h o n l y a p p l y i n g r e s o l u t i o n a s a r u l e i n a n a v e m a n n e r i s t h a t t h e n u m b e r o f n e w c l a u s e s g e n e r a t e d c a n r a p i d l y g r o w t o a n e n o r m o u s s i z e a n d t h i s i s p a r t i c u l a r l y t r u e w h e r e t h e c l a u s e s a r e e n c o d i n g e q u a l i t y a s a l o g i c a l c o n c e p t . O n e a n s w e r i s t o t r e a t e q u a l i t y a s a s p e c i a l c a s e .
O t h e r i m p r o v e m e n t s t o m a k e p r o v e r s p r a c t i c a l a r e t o i m p o s e o r d e r o n t h e p a r t s o f t h e l o g i c a l e x p r e s s i o n ( l i t e r a l s a n d t e r m s ) , u s e a s e t o f r u l e s r a t h e r t h a n j u s t r e s o l u t i o n a n d r e m o v e r e d u n d a n t c l a u s e s e f f i c i e n t l y a t a n e a r l y s t a g e .
A n e f f i c i e n t s o l v e r u s i n g s u c h a n a p p r o a c h i s E w r i t t e n m a i n l y b y S t e p h a n S c h u l z a t M u n i c h . T h i s i s t h e p r o v e r t h a t I h a v e b e e n w o r k i n g w i t h . 2 H D 1 D H
0 1 )2*
A P r o o f i n R o b b i n s A l g e b r a A S u c c e s s f o r A u t o m a t e d T h e o r e m P r o v i n g ! F 2 F E D
0 \[ +2f0
H Despite becoming increasingly sophisticated and useful in a range of fields such as software verification and security protocols, automated theorem proving has not become a tool for mathematicians in the way that computer algebra packages have. A notable exception was the proof in 1996 by McCune of a conjecture by Robbins in Boolean algebra which had eluded human mathematicians for over sixty years. This story made the New York Times.
Though the likes of Andrew Wiles are probably safe for the time being, the original aim of theorem proving, to do maths, has been given a fillip. I 2 I H D
0 ] 021
T M a c h i n e L e a r n i n g S u p p o r t V e c t o r M a c h i n e s + 2 + * D m
0 g 12;
k Machine learning involves using a computer to find a relationship between measurable features of a problem (eg temperature of a patient etc) and some outcome, typically a classification (the patient has measles or does not have measles). Rather than analytically model the relationship; instead, parameter values in a model are estimated by looking at historic data (the learning process). If this is done correctly, the same parameters can be used to classify previously unseen data.
In a support vector machine the numerical values are transformed to new values in a multi-dimensional space which may be of different dimension to the original feature set. In the new space the values can be partitioned in a linear fashion and classification is determined by which side of the partition a transformed point lies.
Following advice from Sean Holden, an expert in the field, I have so far used the program SVMlite to generate classifiers in the form of support vector machines. At the same time I have passed the data on to Sean Holden and Andrew Naish at the Cambridge Computer Lab who are able to apply more sophisticated methods. l 2 l Z l Q D
0 s ;2<
~ Finding Features in Proof States ! 2 ! D
0 D -=2*D
I n t h e o r e m p r o v i n g a p r o o f s t a t e i s t h e c o l l e c t i o n o f l o g i c a l c l a u s e s , d i v i d e d i n t o p r o c e s s e d a n d u n p r o c e s s e d s e t s , t h a t p r o v i d e a s n a p s h o t o f t h e p r o o f p r o c e s s . T h e i n i t i a l p r o o f s t a t e g e n e r a l l y c o n s i s t s o f t h e n e g a t e d t h e o r e m t o b e p r o v e d t o g e t h e r w i t h t h e a s s o c i a t e d a x i o m s a l l o f w h i c h a r e i n a n u n p r o c e s s e d s t a t e . A s t h e s e a r c h f o r a p r o o f p r o g r e s s e s t h e n u m b e r o f c l a u s e s i n c r e a s e s a n d s o m e a r e m o v e d t o a p r o c e s s e d s e t . T h e p r o o f s t a t e a l s o c o n t a i n s i n f o r m a t i o n a s t o h o w t h e g e n e r a t e d c l a u s e s a r o s e .
T o a p p l y m a c h i n e l e a r n i n g t o t h e o r e m p r o v i n g r e q u i r e s a m e a n s o f m e a s u r i n g f e a t u r e s i n t h e p r o o f s t a t e , e i t h e r f o r t h e o r i g i n a l t h e o r e m a n d a x i o m s o r b y r u n n i n g t h e p r o v e r f o r a s h o r t w h i l e t o r e a c h a m o r e c o m p l e x p r o o f s t a t e . P o s s i b l e f e a t u r e s a r e c l a u s e r e l a t e d ( e g c l a u s e l e n g t h ) , o r i n v o l v e w h o l e s e t s o f c l a u s e s .
M y i n i t i a l r u n s u s e d 1 6 f e a t u r e s , t h e n u m b e r w a s i n c r e a s e d t o 6 0 i n l a t e r r u n s . 2 H ^ D
0 J3[
2 James Bridge supervised by Professor Larry Paulson 3 ( 2 3 2 D P
C ( A C U n i b i g '
0 D2E
n Acknowledgements 2 D
0 6F2wH
, I have received much guidance from my supervisor Larry Paulson and from Sean Holden. Andrew Naish has analysed the data I have generated using his own software and Stephan Schulz, the author of E has provided ideas and patiently answered my e-mails despite having a full-time job outside of academia. - 2 - . \ D
!
0 ( 6C
P Working with approximately 1200 theorems in the SET classification of the TPTP library led to a classifier that was correct 70% of the time but the sample was skewed so the base line would be 57%. The tentative conclusion is that useful results may be obtained from machine learning but that more work is needed on feature selection and learning methods.
Rather than remain with classifying theorems into solvable or not, the new work will be applied to the more useful area of heuristic selection. 2 D
"
0 Pt "#2#
v Applying Theorem Proving 2 D
#
0 Ht $2(
z T h e o b v i o u s a n d o r i g i n a l a p p l i c a t i o n i s c h e c k i n g m a t h e m a t i c a l t h e o r e m s a s a t o o l f o r m a t h e m a t i c i a n s b u t t h i s h a s p r o v e d a n e l u s i v e g o a l ( w i t h s o m e e x c e p t i o n s o n e o f w h i c h i s d e s c r i b e d b e l o w ) . B u t t h e o r e m p r o v e r s c a n b e a p p l i e d t o a n y p r o b l e m w h e r e y o u w a n t t o p r o v e t h a t a c o m p l i c a t e d p r o c e s s d o e s n t a l t e r s o m e d e s i r e d i n v a r i a n t o r a n o u t c o m e f o l l o w s f r o m t h e i n p u t c o n d i t i o n s . C o m p u t e r s o f t w a r e a n d h a r d w a r e a r e o b v i o u s c a n d i d a t e s b u t o t h e r a p p l i c a t i o n s i n c l u d e s e c u r i t y p r o t o c o l s ( f o r e x a m p l e C o h e n s T A P S s y s t e m ) , c o m m o n s e n s e r e a s o n i n g i n A I a n d e v e n g e o m e t r i c p r o o f s a n d t h e g e n e r a t i o n o f c o n s i s t e n t t h r e e d i m e n s i o n a l m o d e l s f r o m i m a g e s . 2 . D L B
$
c $ D J L B
%
c $ D L3L3J H
0 nF! ? 33 8 0 _ _ _ P P T 1 0 . r rM Q NM 1 ( 4 J
b / 0 D A r i a l N e w R o m a n L L Ԗ 0Ԗ " D T i m e s N e w R o m a n L L Ԗ 0Ԗ @ . D
@ n ? " d d @ @@ ``
՜. +,0
x Custom þ ) Arial Times New Roman Default Design 7 Applying Machine Learning to Automatic Theorem Proving Fonts Used Design Template
Slide Titles $ _㟾 James Bridge J a m e s B r i d g e i t y a s a l o g i c a l c o n c e p t . O n e a n s w e r i s t o t r e a t e q u a l i t y a s a s p e c i a l c a s e .
O t h e r i m p r o v e m e n t s t o m a k e p r o v e r s p r a c t i c a l a r e t o i m p o s e o r d e r o n t h e p a r t s o f t h e l o g i c a l e x p r e s s i o n ( l i t e r a l s a n d t e r m s ) , u s e a s e t o f r u l e s r a t h e r t h a n j u s t r e s o l u t i o n a n d r e m o v e r e d u n d a n t c l a u s e s e f f i c i e n t l y a t a n e a r l y s t a g e .
A n e f f i c i e n t s o l v e r u s i n g s u c h a n a p p r o a c h i s E w r i t t e n m a i n l y b y S t e p h a n S c h u l z a t M u n i c h . T h i s i s t h e p r o v e r t h a t I h a v e b e e n w o r k i n g w i t h . 2 H D 1 D H
0 1 )2*
A P r o o f i n R o b b i n s A l g e b r a A S u c c e s s f o r A u t o m a t e d T h e o r e m P r o v i n g ! F 2 F E D
0 \[ +2f0
H Despite becoming increasingly sophisticated and useful in a range of fields such as software verification and security protocols, automated theorem proving has not become a tool for mathematicians in the way that computer algebra packages have. A notable exception was the proof in 1996 by McCune of a conjecture by Robbins in Boolean algebra which had eluded human mathematicians for over sixty years. This story made the New York Times.
Though the likes of Andrew Wiles are probably safe for the time being, the original aim of theorem proving, to do maths, has been given a fillip. I 2 I H D
0 ] 021
T M a c h i n e L e a r n i n g S u p p o r t V e c t o r M a c h i n e s + 2 + * D i
0 g 12;
g Machine learning involves using a computer to find a relationship between measurable features of a problem (eg temperature of a patient etc) and some outcome, typically a classification (the patient has measles or does not have measles). Rather than analytically model the relationship; instead, parameter values in a model are estimated by looking at historic data (the learning process). If this is done correctly, the same parameters can be used to classify previously unseen data.
In a support vector machine the numerical values are transformed to new values in a multi-dimensional space which may be of different dimension to the original feature set. In the new space the values can be partitioned in a linear fashion and classification is determined by which side of the partition a transformed point lies.
Following advice from Sean Holden, an expert in the field, I have so far used the program SVMlite to generate classifiers in the form of support vector machines. At the same time I have passed the data on to Sean and to Andrew Naish at the Cambridge Computer Lab who are able to apply more sophisticated methods. h 2 h Z l Q D
0 s ;2<
~ Finding Features in Proof States ! 2 ! D
0 D -=2*D
I n t h e o r e m p r o v i n g a p r o o f s t a t e i s t h e c o l l e c t i o n o f l o g i c a l c l a u s e s , d i v i d e d i n t o p r o c e s s e d a n d u n p r o c e s s e d s e t s , t h a t p r o v i d e a s n a p s h o t o f t h e p r o o f p r o c e s s . T h e i n i t i a l p r o o f s t a t e g e n e r a l l y c o n s i s t s o f t h e n e g a t e d t h e o r e m t o b e p r o v e d t o g e t h e r w i t h t h e a s s o c i a t e d a x i o m s a l l o f w h i c h a r e i n a n u n p r o c e s s e d s t a t e . A s t h e s e a r c h f o r a p r o o f p r o g r e s s e s t h e n u m b e r o f c l a u s e s i n c r e a s e s a n d s o m e a r e m o v e d t o a p r o c e s s e d s e t . T h e p r o o f s t a t e a l s o c o n t a i n s i n f o r m a t i o n a s t o h o w t h e g e n e r a t e d c l a u s e s a r o s e .
T o a p p l y m a c h i n e l e a r n i n g t o t h e o r e m p r o v i n g r e q u i r e s a m e a n s o f m e a s u r i n g f e a t u r e s i n t h e p r o o f s t a t e , e i t h e r f o r t h e o r i g i n a l t h e o r e m a n d a x i o m s o r b y r u n n i n g t h e p r o v e r f o r a s h o r t w h i l e t o r e a c h a m o r e c o m p l e x p r o o f s t a t e . P o s s i b l e f e a t u r e s a r e c l a u s e r e l a t e d ( e g c l a u s e l e n g t h ) , o r i n v o l v e w h o l e s e t s o f c l a u s e s .
M y i n i t i a l r u n s u s e d 1 6 f e a t u r e s , t h e n u m b e r w a s i n c r e a s e d t o 6 0 i n l a t e r r u n s . 2 H ^ D
0 J3[
2 James Bridge supervised by Professor Larry Paulson 3 ( 2 3 2 D P
C ( A C U n i b i g '
0 D2E
n Acknowledgements 2 D
0 6F2wH
, I have received much guidance from my supervisor Larry Paulson and from Sean Holden. Andrew Naish has analysed the data I have generated using his own software and Stephan Schulz, the author of E has provided ideas and patiently answered my e-mails despite having a full-time job outside of academia. - 2 - . \ D
!
0 ( 6C
P Working with approximately 1200 theorems in the SET classification of the TPTP library led to a classifier that was correct 70% of the time but the sample was skewed so the base line would be 57%. The tentative conclusion is that useful results may be obtained from machine learning but that more work is needed on feature selection and learning methods.
Rather than remain with classifying theorems into solvable or not, the new work will be applied to the more useful area of heuristic selection. 2 D
"
0 Pt "#2#
v Applying Theorem Proving 2 D
#
0 Ht $2(
z T h e o b v i o u s a n d o r i g i n a l a p p l i c a t i o n i s c h e c k i n g m a t h e m a t i c a l t h e o r e m s a s a t o o l f o r m a t h e m a t i c i a n s b u t t h i s h a s p r o v e d a n e l u s i v e g o a l ( w i t h s o m e e x c e p t i o n s o n e o f w h i c h i s d e s c r i b e d b e l o w ) . B u t t h e o r e m p r o v e r s c a n b e a p p l i e d t o a n y p r o b l e m w h e r e y o u w a n t t o p r o v e t h a t a c o m p l i c a t e d p r o c e s s d o e s n t a l t e r s o m e d e s i r e d i n v a r i a n t o r a n o u t c o m e f o l l o w s f r o m t h e i n p u t c o n d i t i o n s . C o m p u t e r s o f t w a r e a n d h a r d w a r e a r e o b v i o u s c a n d i d a t e s b u t o t h e r a p p l i c a t i o n s i n c l u d e s e c u r i t y p r o t o c o l s ( f o r e x a m p l e C o h e n s T A P S s y s t e m ) , c o m m o n s e n s e r e a s o n i n g i n A I a n d e v e n g e o m e t r i c p r o o f s a n d t h e g e n e r a t i o n o f c o n s i s t e n t t h r e e d i m e n s i o n a l m o d e l s f r o m i m a g e s . 2 . D H
0 nF! ? 33 8 0 _ _ _ P P T 1 0 . r Q ܚ - H 1 ( 4 J
b / 0 D A r i a l N e w R o m a n L L Ԗ 0Ԗ " D T i m e s N e w R o m a n L L Ԗ 0Ԗ @ . D
@ n ? " d d @ @@ `` ' # ' , 2 $ /4@DeFY,-KG dS 0 A A @ 3 ʚ; ʚ; g 4 2 d 2 d d 0 p A% p P < 4 d d d d A10L 8 0 _ _ _ P P T 1 0
p p 6 Applying Machine Learning to Automatic Theorem Proving 7 7 B 6
KD 0 C C & KC (
x
c $ t < 4p
0 ( 5
{ The Nature of the Research 2 D p
0 ]
The aim of my research is to use machine learning techniques to detect patterns within logical theorems and use them to guide automated theorem provers. 2 . D
0 Э h ]
$ The Intended Outcome of the Research % 2 % $ D
0 !'
N The primary aim is to extend the range of theorems that can be proved automatically in reasonable time.
A secondary aim is to develop an understanding of structure within theorems and how this may be exploited in theorem proving heuristics. 2 D
0 H (] *
~ The Present Status of the Work 2 D
0 p 7* 4
x I n i n i t i a l e x p e r i m e n t s I v e r u n t h e o r e m p r o v e r f o r a s h o r t t i m e , c o l l e c t e d d a t a , t h e n r u n t o c o m p l e t i o n . I a p p l i e d m a c h i n e l e a r n i n g t o g e n e r a t e a c l a s s i f i e r t o p r e d i c t w h e t h e r o r n o t a t h e o r e m w i l l b e p r o v e d w i t h o u t n e e d i n g t o r u n t h e p r o o f p r o c e s s t o c o m p l e t i o n . R e s u l t s a r e p r o m i s i n g b u t i n c o n c l u s i v e . I n o w p l a n t o e x t e n d t h e w o r k t o l e a r n i n g h e u r i s t i c s e l e c t i o n f r o m t h e o r e m d a t a . 2 . ( R D
0 ]e
} The Challenge to be Addressed 2 D
0 t c
Using computers to search for logical proofs of theorems has many applications ranging from pure maths to hardware and software verification. But the power of computer theorem provers falls well short of the initial promise of early work. The main challenge is the enormous size of the search space containing the proof being looked for. Much progress in search heuristics has been made but different heuristics work better with different theorems and determining which heuristic to pick for a new theorem is not straight forward. 2 . [ D
0 < 4]F6
# Preliminary Results and Conclusions $ 2 $ # D
0 l 2
! Logic Systems and Theorem Provers " 2 " " D q
0
2
g In logic there is a trade off between expressive power in stating theorems and the decidability of the proof process.
The simplest logic is propositional logic where theorems are Boolean expressions and the proof process is described as satisfiability or SAT. SAT is decidable but propositional logic is too simple to express many mathematical ideas and problems. Even at this level, for general expressions SAT is NP-complete and there is unlikely to be a polynomial time algorithm to solve it.
First order logic adds existential and universal quantifiers and allows functions so is significantly more powerful than propositional logic. It is semi-decidable. Most automatic theorem provers work in first order logic.
Beyond first order logic, higher order logics are widely used and are particularly useful for expressing complex hardware and software verification conditions but cannot generally be solved automatically. Instead proof assistants are used which require expert human intervention in the process.
Much work is being done on combining automated first order logic provers with higher order logic proof assistants. h 2 h b * D
0 2s
* Automatic Theorem Proving and the E-prover + 2 + " $ D 2
0 + 2!
B A u t o m a t e d t h e o r e m p r o v i n g d o e s n o t r e p r o d u c e t h e c o m p l e x b u t r e l a t i v e l y s h o r t p r o o f s t h a t h u m a n m a t h e m a t i c i a n s p r o d u c e . I n s t e a d s i m p l e l o g i c r u l e s a r e a p p l i e d t o m a n y c l a u s e s u n t i l a c o n t r a d i c t i o n i s r e a c h e d . T h e o r e m s a r e p r o v e d b y d e m o n s t r a t i n g a c o n t r a d i c t i o n i f t h e n e g a t i o n o f t h e t h e o r e m i s a s s u m e d . O n e s u c h r u l e t h a t m a y b e a p p l i e d i s r e s o l u t i o n ( s h o w e d t o b e c o m p l e t e a n d s o u n d i n 1 9 6 5 b y R o b i n s o n ) . T h o u g h m o r e c o m p l i c a t e d r u l e s a r e n o w a p p l i e d , s u c h s o l v e r s a r e o f t e n d e s c r i b e d a s b e i n g r e s o l u t i o n b a s e d .
T h e p r o b l e m w i t h o n l y a p p l y i n g r e s o l u t i o n a s a r u l e i n a n a v e m a n n e r i s t h a t t h e n u m b e r o f n e w c l a u s e s g e n e r a t e d c a n r a p i d l y g r o w t o a n e n o r m o u s s i z e a n d t h i s i s p a r t i c u l a r l y t r u e w h e r e t h e c l a u s e s a r e e n c o d i n g e q u a l i t y a s a l o g i c a l c o n c e p t . O n e a n s w e r i s t o t r e a t e q u a l i t y a s a s p e c i a l c a s e .
O t h e r i m p r o v e m e n t s t o m a k e p r o v e r s p r a c t i c a l a r e t o i m p o s e o r d e r o n t h e p a r t s o f t h e l o g i c a l e x p r e s s i o n ( l i t e r a l s a n d t e r m s ) , u s e a s e t o f r u l e s r a t h e r t h a n j u s t r e s o l u t i o n a n d r e m o v e r e d u n d a n t c l a u s e s e f f i c i e n t l y a t a n e a r l y s t a g e .
A n e f f i c i e n t s o l v e r u s i n g s u c h a n a p p r o a c h i s E w r i t t e n m a i n l y b y S t e p h a n S c h u l z a t M u n i c h . T h i s i s t h e p r o v e r t h a t I h a v e b e e n w o r k i n g w i t h . 2 H D 1 D H
0 1 )2*
A P r o o f i n R o b b i n s A l g e b r a A S u c c e s s f o r A u t o m a t e d T h e o r e m P r o v i n g ! F 2 F E D
0 \[ +2f0
H Despite becoming increasingly sophisticated and useful in a range of fields such as software verification and security protocols, automated theorem proving has not become a tool for mathematicians in the way that computer algebra packages have. A notable exception was the proof in 1996 by McCune of a conjecture by Robbins in Boolean algebra which had eluded human mathematicians for over sixty years. This story made the New York Times.
Though the likes of Andrew Wiles are probably safe for the time being, the original aim of theorem proving, to do maths, has been given a fillip. I 2 I H D
0 ] 021
T M a c h i n e L e a r n i n g S u p p o r t V e c t o r M a c h i n e s + 2 + * D i
0 g 12;
g Machine learning involves using a computer to find a relationship between measurable features of a problem (eg temperature of a patient etc) and some outcome, typically a classification (the patient has measles or does not have measles). Rather than analytically model the relationship; instead, parameter values in a model are estimated by looking at historic data (the learning process). If this is done correctly, the same parameters can be used to classify previously unseen data.
In a support vector machine the numerical values are transformed to new values in a multi-dimensional space which may be of different dimension to the original feature set. In the new space the values can be partitioned in a linear fashion and classification is determined by which side of the partition a transformed point lies.
Following advice from Sean Holden, an expert in the field, I have so far used the program SVMlite to generate classifiers in the form of support vector machines. At the same time I have passed the data on to Sean and to Andrew Naish at the Cambridge Computer Lab who are able to apply more sophisticated methods. h 2 h Z l Q D
0 s ;2<
~ Finding Features in Proof States ! 2 ! D
0 D -=2*D
I n t h e o r e m p r o v i n g a p r o o f s t a t e i s t h e c o l l e c t i o n o f l o g i c a l c l a u s e s , d i v i d e d i n t o p r o c e s s e d a n d u n p r o c e s s e d s e t s , t h a t p r o v i d e a s n a p s h o t o f t h e p r o o f p r o c e s s . T h e i n i t i a l p r o o f s t a t e g e n e r a l l y c o n s i s t s o f t h e n e g a t e d t h e o r e m t o b e p r o v e d t o g e t h e r w i t h t h e a s s o c i a t e d a x i o m s a l l o f w h i c h a r e i n a n u n p r o c e s s e d s t a t e . A s t h e s e a r c h f o r a p r o o f p r o g r e s s e s t h e n u m b e r o f c l a u s e s i n c r e a s e s a n d s o m e a r e m o v e d t o a p r o c e s s e d s e t . T h e p r o o f s t a t e a l s o c o n t a i n s i n f o r m a t i o n a s t o h o w t h e g e n e r a t e d c l a u s e s a r o s e .
T o a p p l y m a c h i n e l e a r n i n g t o t h e o r e m p r o v i n g r e q u i r e s a m e a n s o f m e a s u r i n g f e a t u r e s i n t h e p r o o f s t a t e , e i t h e r f o r t h e o r i g i n a l t h e o r e m a n d a x i o m s o r b y r u n n i n g t h e p r o v e r f o r a s h o r t w h i l e t o r e a c h a m o r e c o m p l e x p r o o f s t a t e . P o s s i b l e f e a t u r e s a r e c l a u s e r e l a t e d ( e g c l a u s e l e n g t h ) , o r i n v o l v e w h o l e s e t s o f c l a u s e s .
M y i n i t i a l r u n s u s e d 1 6 f e a t u r e s , t h e n u m b e r w a s i n c r e a s e d t o 6 0 i n l a t e r r u n s . 2 H ^ D
0 J3[
2 James Bridge supervised by Professor Larry Paulson 3 ( 2 3 2 D P
C ( A C U n i b i g '
0 D2E
n Acknowledgements 2 D
0 6F2wH
, I have received much guidance from my supervisor Larry Paulson and from Sean Holden. Andrew Naish has analysed the data I have generated using his own software and Stephan Schulz, the author of E has provided ideas and patiently answered my e-mails despite having a full-time job outside of academia. - 2 - . \ D
!
0 ( 6C
P Working with approximately 1200 theorems in the SET classification of the TPTP library led to a classifier that was correct 70% of the time but the sample was skewed so the base line would be 57%. The tentative conclusion is that useful results may be obtained from machine learning but that more work is needed on feature selection and learning methods.
Rather than remain with classifying theorems into solvable or not, the new work will be applied to the more useful area of heuristic selection. 2 D
"
0 Pt "#2#
v Applying Theorem Proving 2 D
#
0 Ht $2(
z T h e o b v i o u s a n d o r i g i n a l a p p l i c a t i o n i s c h e c k i n g m a t h e m a t i c a l t h e o r e m s a s a t o o l f o r m a t h e m a t i c i a n s b u t t h i s h a s p r o v e d a n e l u s i v e g o a l ( w i t h s o m e e x c e p t i o n s o n e o f w h i c h i s d e s c r i b e d b e l o w ) . B u t t h e o r e m p r o v e r s c a n b e a p p l i e d t o a n y p r o b l e m w h e r e y o u w a n t t o p r o v e t h a t a c o m p l i c a t e d p r o c e s s d o e s n t a l t e r s o m e d e s i r e d i n v a r i a n t o r a n o u t c o m e f o l l o w s f r o m t h e i n p u t c o n d i t i o n s . C o m p u t e r s o f t w a r e a n d h a r d w a r e a r e o b v i o u s c a n d i d a t e s b u t o t h e r a p p l i c a t i o n s i n c l u d e s e c u r i t y p r o t o c o l s ( f o r e x a m p l e C o h e n s T A P S s y s t e m ) , c o m m o n s e n s e r e a s o n i n g i n A I a n d e v e n g e o m e t r i c p r o o f s a n d t h e g e n e r a t i o n o f c o n s i s t e n t t h r e e d i m e n s i o n a l m o d e l s f r o m i m a g e s . 2 . D
&
0 9I/ 3I
5th June 2007 , 2
D H
0 nF! ? 33 8 0 _ _ _ P P T 1 0 . r ` b' 1 ( 4 J
b / 0 D A r i a l N e w R o m a n L L Ԗ 0Ԗ " D T i m e s N e w R o m a n L L Ԗ 0Ԗ @ . D
@ n ? " d d @ @@ `` ' # ' , 2 $ /4@DeFY,-KG dS 0 A A @ 3 ʚ; ʚ; g 4 2 d 2 d d 0 p A% p P < 4 d d d d A10L 8 0 _ _ _ P P T 1 0
p p 6 Applying Machine Learning to Automatic Theorem Proving 7 7 B 6
r ' z' ), 1 ( 4 J
b / 0 D A r i a l N e w R o m a n L L Ԗ 0Ԗ D T i m e s N e w R o m a n L L Ԗ 0Ԗ @ . D
@ n ? " d d @ @@ `` ' # ' , 2 $ /4@DeFY,-KG dS 0 A A @ 3 ʚ; ʚ; g 4 2 d 2 d `, 0 p A% p P < 4 d d d d A10L 8 0 _ _ _ P P T 1 0
p p 6 Applying Machine Learning to Automatic Theorem Proving 7 7 B 6
sD 0 C C & sC (
x
c $ Ǒ < 4p
0 xґ 5
{ The Nature of the Research 2 D p
0 ԑ ]
The aim of my research is to use machine learning techniques to detect patterns within logical theorems and use them to guide automated theorem provers. 2 . D
0 h ]
$ The Intended Outcome of the Research % 2 % $ D
0 !'
N The primary aim is to extend the range of theorems that can be proved automatically in reasonable time.
A secondary aim is to develop an understanding of structure within theorems and how this may be exploited in theorem proving heuristics. 2 D
0 D6 (] *
~ The Present Status of the Work 2 D
0 |6 7* 4
I n i n i t i a l e x p e r i m e n t s I v e r u n a t h e o r e m p r o v e r f o r a s h o r t t i m e , c o l l e c t e d d a t a , t h e n r u n t o c o m p l e t i o n . I t h e n a p p l i e d m a c h i n e l e a r n i n g t o g e n e r a t e a c l a s s i f i e r t o p r e d i c t w h e t h e r o r n o t a t h e o r e m w i l l b e p r o v e d w i t h o u t n e e d i n g t o r u n t h e p r o o f p r o c e s s t o c o m p l e t i o n . R e s u l t s a r e p r o m i s i n g b u t i n c o n c l u s i v e . I n o w p l a n t o e x t e n d t h e w o r k t o l e a r n i n g h e u r i s t i c s e l e c t i o n f r o m t h e o r e m d a t a . 2 H * = D
0 x6 ]e
} The Challenge to be Addressed 2 D
0 h6 c
Using computers to search for logical proofs of theorems has many applications ranging from pure maths to hardware and software verification. But the power of computer theorem provers falls well short of the initial promise of early work. The main challenge is the enormous size of the search space containing the proof being looked for. Much progress in search heuristics has been made but different heuristics work better with different theorems and determining which heuristic to pick for a new theorem is not straight forward. 2 . [ D
0 $6 4]F6
# Preliminary Results and Conclusions $ 2 $ # D
0 26 2
! Logic Systems and Theorem Provers " 2 " " D q
0 <6 2
g In logic there is a trade off between expressive power in stating theorems and the decidability of the proof process.
The simplest logic is propositional logic where theorems are Boolean expressions and the proof process is described as satisfiability or SAT. SAT is decidable but propositional logic is too simple to express many mathematical ideas and problems. Even at this level, for general expressions SAT is NP-complete and there is unlikely to be a polynomial time algorithm to solve it.
First order logic adds existential and universal quantifiers and allows functions so is significantly more powerful than propositional logic. It is semi-decidable. Most automatic theorem provers work in first order logic.
Beyond first order logic, higher order logics are widely used and are particularly useful for expressing complex hardware and software verification conditions but cannot generally be solved automatically. Instead proof assistants are used which require expert human intervention in the process.
Much work is being done on combining automated first order logic provers with higher order logic proof assistants. h 2 h b * D
0 H6 2s
* Automatic Theorem Proving and the E-prover + 2 + " $ D 2
0 \6 2!
B A u t o m a t e d t h e o r e m p r o v i n g d o e s n o t r e p r o d u c e t h e c o m p l e x b u t r e l a t i v e l y s h o r t p r o o f s t h a t h u m a n m a t h e m a t i c i a n s p r o d u c e . I n s t e a d s i m p l e l o g i c r u l e s a r e a p p l i e d t o m a n y c l a u s e s u n t i l a c o n t r a d i c t i o n i s r e a c h e d . T h e o r e m s a r e p r o v e d b y d e m o n s t r a t i n g a c o n t r a d i c t i o n i f t h e n e g a t i o n o f t h e t h e o r e m i s a s s u m e d . O n e s u c h r u l e t h a t m a y b e a p p l i e d i s r e s o l u t i o n ( s h o w e d t o b e c o m p l e t e a n d s o u n d i n 1 9 6 5 b y R o b i n s o n ) . T h o u g h m o r e c o m p l i c a t e d r u l e s a r e n o w a p p l i e d , s u c h s o l v e r s a r e o f t e n d e s c r i b e d a s b e i n g r e s o l u t i o n b a s e d .
T h e p r o b l e m w i t h o n l y a p p l y i n g r e s o l u t i o n a s a r u l e i n a n a v e m a n n e r i s t h a t t h e n u m b e r o f n e w c l a u s e s g e n e r a t e d c a n r a p i d l y g r o w t o a n e n o r m o u s s i z e a n d t h i s i s p a r t i c u l a r l y t r u e w h e r e t h e c l a u s e s a r e e n c o d i n g e q u a l i t y a s a l o g i c a l c o n c e p t . O n e a n s w e r i s t o t r e a t e q u a l i t y a s a s p e c i a l c a s e .
O t h e r i m p r o v e m e n t s t o m a k e p r o v e r s p r a c t i c a l a r e t o i m p o s e o r d e r o n t h e p a r t s o f t h e l o g i c a l e x p r e s s i o n ( l i t e r a l s a n d t e r m s ) , u s e a s e t o f r u l e s r a t h e r t h a n j u s t r e s o l u t i o n a n d r e m o v e r e d u n d a n t c l a u s e s e f f i c i e n t l y a t a n e a r l y s t a g e .
A n e f f i c i e n t s o l v e r u s i n g s u c h a n a p p r o a c h i s E w r i t t e n m a i n l y b y S t e p h a n S c h u l z a t M u n i c h . T h i s i s t h e p r o v e r t h a t I h a v e b e e n w o r k i n g w i t h . 2 H D 1 D H
0 x6 )2*
A P r o o f i n R o b b i n s A l g e b r a A S u c c e s s f o r A u t o m a t e d T h e o r e m P r o v i n g ! F 2 F E D
0 Ԋ6 +2f0
H Despite becoming increasingly sophisticated and useful in a range of fields such as software verification and security protocols, automated theorem proving has not become a tool for mathematicians in the way that computer algebra packages have. A notable exception was the proof in 1996 by McCune of a conjecture by Robbins in Boolean algebra which had eluded human mathematicians for over sixty years. This story made the New York Times.
Though the likes of Andrew Wiles are probably safe for the time being, the original aim of theorem proving, to do maths, has been given a fillip. I 2 I H D
0 6 021
T M a c h i n e L e a r n i n g S u p p o r t V e c t o r M a c h i n e s + 2 + * D i
0 d6 12;
g Machine learning involves using a computer to find a relationship between measurable features of a problem (eg temperature of a patient etc) and some outcome, typically a classification (the patient has measles or does not have measles). Rather than analytically model the relationship; instead, parameter values in a model are estimated by looking at historic data (the learning process). If this is done correctly, the same parameters can be used to classify previously unseen data.
In a support vector machine the numerical values are transformed to new values in a multi-dimensional space which may be of different dimension to the original feature set. In the new space the values can be partitioned in a linear fashion and classification is determined by which side of the partition a transformed point lies.
Following advice from Sean Holden, an expert in the field, I have so far used the program SVMlite to generate classifiers in the form of support vector machines. At the same time I have passed the data on to Sean and to Andrew Naish at the Cambridge Computer Lab who are able to apply more sophisticated methods. h 2 h Z l Q D
0 6 ;2<
~ Finding Features in Proof States ! 2 ! D
0 6 -=2*D
I n t h e o r e m p r o v i n g a p r o o f s t a t e i s t h e c o l l e c t i o n o f l o g i c a l c l a u s e s , d i v i d e d i n t o p r o c e s s e d a n d u n p r o c e s s e d s e t s , t h a t p r o v i d e a s n a p s h o t o f t h e p r o o f p r o c e s s . T h e i n i t i a l p r o o f s t a t e g e n e r a l l y c o n s i s t s o f t h e n e g a t e d t h e o r e m t o b e p r o v e d t o g e t h e r w i t h t h e a s s o c i a t e d a x i o m s a l l o f w h i c h a r e i n a n u n p r o c e s s e d s t a t e . A s t h e s e a r c h f o r a p r o o f p r o g r e s s e s t h e n u m b e r o f c l a u s e s i n c r e a s e s a n d s o m e a r e m o v e d t o a p r o c e s s e d s e t . T h e p r o o f s t a t e a l s o c o n t a i n s i n f o r m a t i o n a s t o h o w t h e g e n e r a t e d c l a u s e s a r o s e .
T o a p p l y m a c h i n e l e a r n i n g t o t h e o r e m p r o v i n g r e q u i r e s a m e a n s o f m e a s u r i n g f e a t u r e s i n t h e p r o o f s t a t e , e i t h e r f o r t h e o r i g i n a l t h e o r e m a n d a x i o m s o r b y r u n n i n g t h e p r o v e r f o r a s h o r t w h i l e t o r e a c h a m o r e c o m p l e x p r o o f s t a t e . P o s s i b l e f e a t u r e s a r e c l a u s e r e l a t e d ( e g c l a u s e l e n g t h ) , o r i n v o l v e w h o l e s e t s o f c l a u s e s .
M y i n i t i a l r u n s u s e d 1 6 f e a t u r e s , t h e n u m b e r w a s i n c r e a s e d t o 6 0 i n l a t e r r u n s . 2 H ^ D
0 6 J3[
2 James Bridge supervised by Professor Larry Paulson 3 ( 2 3 2 D P
C ( A C U n i b i g '
0 H6 D2E
n Acknowledgements 2 D
0 6 6F2wH
, I have received much guidance from my supervisor Larry Paulson and from Sean Holden. Andrew Naish has analysed the data I have generated using his own software and Stephan Schulz, the author of E has provided ideas and patiently answered my e-mails despite having a full-time job outside of academia. - 2 - . \ D
!
0 X6 6C
P Working with approximately 1200 theorems in the SET classification of the TPTP library led to a classifier that was correct 70% of the time but the sample was skewed so the base line would be 57%. The tentative conclusion is that useful results may be obtained from machine learning but that more work is needed on feature selection and learning methods.
Rather than remain with classifying theorems into solvable or not, the new work will be applied to the more useful area of heuristic selection. 2 D
"
0 7 "#2#
v Applying Theorem Proving 2 D
#
0 7 $2(
z T h e o b v i o u s a n d o r i g i n a l a p p l i c a t i o n i s c h e c k i n g m a t h e m a t i c a l t h e o r e m s a s a t o o l f o r m a t h e m a t i c i a n s b u t t h i s h a s p r o v e d a n e l u s i v e g o a l ( w i t h s o m e e x c e p t i o n s o n e o f w h i c h i s d e s c r i b e d b e l o w ) . B u t t h e o r e m p r o v e r s c a n b e a p p l i e d t o a n y p r o b l e m w h e r e y o u w a n t t o p r o v e t h a t a c o m p l i c a t e d p r o c e s s d o e s n t a l t e r s o m e d e s i r e d i n v a r i a n t o r a n o u t c o m e f o l l o w s f r o m t h e i n p u t c o n d i t i o n s . C o m p u t e r s o f t w a r e a n d h a r d w a r e a r e o b v i o u s c a n d i d a t e s b u t o t h e r a p p l i c a t i o n s i n c l u d e s e c u r i t y p r o t o c o l s ( f o r e x a m p l e C o h e n s T A P S s y s t e m ) , c o m m o n s e n s e r e a s o n i n g i n A I a n d e v e n g e o m e t r i c p r o o f s a n d t h e g e n e r a t i o n o f c o n s i s t e n t t h r e e d i m e n s i o n a l m o d e l s f r o m i m a g e s . 2 . D
&
0 |7 9I/ 3I
5th June 2007 , 2
D H
0 nF! ? 33 8 0 _ _ _ P P T 1 0 . r ], 0 9, cu 1 ( 4 J
b / 0 D A r i a l N e w R o m a n L L $ Ԗ 0Ԗ D T i m e s N e w R o m a n L L $ Ԗ 0Ԗ @ . D
@ n ? " d d @ @@ `` ( # ' , 2 $ /4@DeFY,-KG dS 0 A A @ 3 ʚ; ʚ; g 4 2 d 2 d 0 p A% p P < 4 d d d d A10L 8 0 _ _ _ P P T 1 0
p p 6 Applying Machine Learning to Automatic Theorem Proving 7 7 B 6
MD 0 C C & YC (
x
c $ @ < 4p
0 5
{ The Nature of the Research 2 D p
0 ģ ]
The aim of my research is to use machine learning techniques to detect patterns within logical theorems and use them to guide automated theorem provers. 2 . D
0 h ]
$ The Intended Outcome of the Research % 2 % $ D
0 !'
N The primary aim is to extend the range of theorems that can be proved automatically in reasonable time.
A secondary aim is to develop an understanding of structure within theorems and how this may be exploited in theorem proving heuristics. 2 D
0 ( (] *
~ The Present Status of the Work 2 D
0 \ 7* 4
I n i n i t i a l e x p e r i m e n t s I v e r u n a t h e o r e m p r o v e r f o r a s h o r t t i m e , c o l l e c t e d d a t a , t h e n r u n t o c o m p l e t i o n . I t h e n a p p l i e d m a c h i n e l e a r n i n g t o g e n e r a t e a c l a s s i f i e r t o p r e d i c t w h e t h e r o r n o t a t h e o r e m w i l l b e p r o v e d w i t h o u t n e e d i n g t o r u n t h e p r o o f p r o c e s s t o c o m p l e t i o n . R e s u l t s a r e p r o m i s i n g b u t i n c o n c l u s i v e . I n o w p l a n t o e x t e n d t h e w o r k t o l e a r n i n g h e u r i s t i c s e l e c t i o n f r o m t h e o r e m d a t a . 2 . * W D
0 0e
} The Challenge to be Addressed 2 D
0 c
Using computers to search for logical proofs of theorems has many applications ranging from pure maths to hardware and software verification. But the power of computer theorem provers falls well short of the initial promise of early work. The main challenge is the enormous size of the search space containing the proof being looked for. Much progress in search heuristics has been made but different heuristics work better with different theorems and determining which heuristic to pick for a new theorem is not straight forward. 2 . [ D
0 D 4]F6
# Preliminary Results and Conclusions $ 2 $ # D
0 < 2
! Logic Systems and Theorem Provers " 2 " " D q
0
2
g In logic there is a trade off between expressive power in stating theorems and the decidability of the proof process.
The simplest logic is propositional logic where theorems are Boolean expressions and the proof process is described as satisfiability or SAT. SAT is decidable but propositional logic is too simple to express many mathematical ideas and problems. Even at this level, for general expressions SAT is NP-complete and there is unlikely to be a polynomial time algorithm to solve it.
First order logic adds existential and universal quantifiers and allows functions so is significantly more powerful than propositional logic. It is semi-decidable. Most automatic theorem provers work in first order logic.
Beyond first order logic, higher order logics are widely used and are particularly useful for expressing complex hardware and software verification conditions but cannot generally be solved automatically. Instead proof assistants are used which require expert human intervention in the process.
Much work is being done on combining automated first order logic provers with higher order logic proof assistants. h 2 h b * D
0 2s
* Automatic Theorem Proving and the E-prover + 2 + " $ D 2
0 . 2!
B A u t o m a t e d t h e o r e m p r o v i n g d o e s n o t r e p r o d u c e t h e c o m p l e x b u t r e l a t i v e l y s h o r t p r o o f s t h a t h u m a n m a t h e m a t i c i a n s p r o d u c e . I n s t e a d s i m p l e l o g i c r u l e s a r e a p p l i e d t o m a n y c l a u s e s u n t i l a c o n t r a d i c t i o n i s r e a c h e d . T h e o r e m s a r e p r o v e d b y d e m o n s t r a t i n g a c o n t r a d i c t i o n i f t h e n e g a t i o n o f t h e t h e o r e m i s a s s u m e d . O n e s u c h r u l e t h a t m a y b e a p p l i e d i s r e s o l u t i o n ( s h o w e d t o b e c o m p l e t e a n d s o u n d i n 1 9 6 5 b y R o b i n s o n ) . T h o u g h m o r e c o m p l i c a t e d r u l e s a r e n o w a p p l i e d , s u c h s o l v e r s a r e o f t e n d e s c r i b e d a s b e i n g r e s o l u t i o n b a s e d .
T h e p r o b l e m w i t h o n l y a p p l y i n g r e s o l u t i o n a s a r u l e i n a n a v e m a n n e r i s t h a t t h e n u m b e r o f n e w c l a u s e s g e n e r a t e d c a n r a p i d l y g r o w t o a n e n o r m o u s s i z e a n d t h i s i s p a r t i c u l a r l y t r u e w h e r e t h e c l a u s e s a r e e n c o d i n g e q u a l i t y a s a l o g i c a l c o n c e p t . O n e a n s w e r i s t o t r e a t e q u a l i t y a s a s p e c i a l c a s e .
O t h e r i m p r o v e m e n t s t o m a k e p r o v e r s p r a c t i c a l a r e t o i m p o s e o r d e r o n t h e p a r t s o f t h e l o g i c a l e x p r e s s i o n ( l i t e r a l s a n d t e r m s ) , u s e a s e t o f r u l e s r a t h e r t h a n j u s t r e s o l u t i o n a n d r e m o v e r e d u n d a n t c l a u s e s e f f i c i e n t l y a t a n e a r l y s t a g e .
A n e f f i c i e n t s o l v e r u s i n g s u c h a n a p p r o a c h i s E w r i t t e n m a i n l y b y S t e p h a n S c h u l z a t M u n i c h . T h i s i s t h e p r o v e r t h a t I h a v e b e e n w o r k i n g w i t h . 2 H D 1 D H
0 1 )2*
A P r o o f i n R o b b i n s A l g e b r a A S u c c e s s f o r A u t o m a t e d T h e o r e m P r o v i n g ! F 2 F E D
0 tN +2f0
H Despite becoming increasingly sophisticated and useful in a range of fields such as software verification and security protocols, automated theorem proving has not become a tool for mathematicians in the way that computer algebra packages have. A notable exception was the proof in 1996 by McCune of a conjecture by Robbins in Boolean algebra which had eluded human mathematicians for over sixty years. This story made the New York Times.
Though the likes of Andrew Wiles are probably safe for the time being, the original aim of theorem proving, to do maths, has been given a fillip. I 2 I H D
0 ] 021
T M a c h i n e L e a r n i n g S u p p o r t V e c t o r M a c h i n e s + 2 + * D i
0 g 12;
g Machine learning involves using a computer to find a relationship between measurable features of a problem (eg temperature of a patient etc) and some outcome, typically a classification (the patient has measles or does not have measles). Rather than analytically model the relationship; instead, parameter values in a model are estimated by looking at historic data (the learning process). If this is done correctly, the same parameters can be used to classify previously unseen data.
In a support vector machine the numerical values are transformed to new values in a multi-dimensional space which may be of different dimension to the original feature set. In the new space the values can be partitioned in a linear fashion and classification is determined by which side of the partition a transformed point lies.
Following advice from Sean Holden, an expert in the field, I have so far used the program SVMlite to generate classifiers in the form of support vector machines. At the same time I have passed the data on to Sean and to Andrew Naish at the Cambridge Computer Lab who are able to apply more sophisticated methods. h 2 h Z l Q D
0 z ;2<
~ Finding Features in Proof States ! 2 ! D
0 , -=2*D
I n t h e o r e m p r o v i n g a p r o o f s t a t e i s t h e c o l l e c t i o n o f l o g i c a l c l a u s e s , d i v i d e d i n t o p r o c e s s e d a n d u n p r o c e s s e d s e t s , t h a t p r o v i d e a s n a p s h o t o f t h e p r o o f p r o c e s s . T h e i n i t i a l p r o o f s t a t e g e n e r a l l y c o n s i s t s o f t h e n e g a t e d t h e o r e m t o b e p r o v e d t o g e t h e r w i t h t h e a s s o c i a t e d a x i o m s a l l o f w h i c h a r e i n a n u n p r o c e s s e d s t a t e . A s t h e s e a r c h f o r a p r o o f p r o g r e s s e s t h e n u m b e r o f c l a u s e s i n c r e a s e s a n d s o m e a r e m o v e d t o a p r o c e s s e d s e t . T h e p r o o f s t a t e a l s o c o n t a i n s i n f o r m a t i o n a s t o h o w t h e g e n e r a t e d c l a u s e s a r o s e .
T o a p p l y m a c h i n e l e a r n i n g t o t h e o r e m p r o v i n g r e q u i r e s a m e a n s o f m e a s u r i n g f e a t u r e s i n t h e p r o o f s t a t e , e i t h e r f o r t h e o r i g i n a l t h e o r e m a n d a x i o m s o r b y r u n n i n g t h e p r o v e r f o r a s h o r t w h i l e t o r e a c h a m o r e c o m p l e x p r o o f s t a t e . P o s s i b l e f e a t u r e s a r e c l a u s e r e l a t e d ( e g c l a u s e l e n g t h ) , o r i n v o l v e w h o l e s e t s o f c l a u s e s .
M y i n i t i a l r u n s u s e d 1 6 f e a t u r e s , t h e n u m b e r w a s i n c r e a s e d t o 6 0 i n l a t e r r u n s . 2 H ^ D
0 J3[
2 James Bridge supervised by Professor Larry Paulson 3 ( 2 3 2 D P
C ( A C U n i b i g '
0 D2E
n Acknowledgements 2 D
0 < 6F2wH
, I have received much guidance from my supervisor Larry Paulson and from Sean Holden. Andrew Naish has analysed the data I have generated using his own software and Stephan Schulz, the author of E has provided ideas and patiently answered my e-mails despite having a full-time job outside of academia. - 2 - . \ D
!
0 6C
P Working with approximately 1200 theorems in the SET classification of the TPTP library led to a classifier that was correct 70% of the time but the sample was skewed so the base line would be 57%. The tentative conclusion is that useful results may be obtained from machine learning but that more work is needed on feature selection and learning methods.
Rather than remain with classifying theorems into solvable or not, the new work will be applied to the more useful area of heuristic selection. 2 D
"
0 tʕ "#2#
v Applying Theorem Proving 2 D
#
0 0ӕ $2(
z T h e o b v i o u s a n d o r i g i n a l a p p l i c a t i o n i s c h e c k i n g m a t h e m a t i c a l t h e o r e m s a s a t o o l f o r m a t h e m a t i c i a n s b u t t h i s h a s p r o v e d a n e l u s i v e g o a l ( w i t h s o m e e x c e p t i o n s o n e o f w h i c h i s d e s c r i b e d b e l o w ) . B u t t h e o r e m p r o v e r s c a n b e a p p l i e d t o a n y p r o b l e m w h e r e y o u w a n t t o p r o v e t h a t a c o m p l i c a t e d p r o c e s s d o e s n t a l t e r s o m e d e s i r e d i n v a r i a n t o r a n o u t c o m e f o l l o w s f r o m t h e i n p u t c o n d i t i o n s . C o m p u t e r s o f t w a r e a n d h a r d w a r e a r e o b v i o u s c a n d i d a t e s b u t o t h e r a p p l i c a t i o n s i n c l u d e s e c u r i t y p r o t o c o l s ( f o r e x a m p l e C o h e n s T A P S s y s t e m ) , c o m m o n s e n s e r e a s o n i n g i n A I a n d e v e n g e o m e t r i c p r o o f s a n d t h e g e n e r a t i o n o f c o n s i s t e n t t h r e e d i m e n s i o n a l m o d e l s f r o m i m a g e s . 2 . D
&
0 9I/ 3I
5th June 2007 , 2
D <
c $ ? 33 8 0 _ _ _ P P T 1 0 . r u 2z {u 1