\setlength{\unitlength}{1740sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
\reset@font\fontsize{#1}{#2pt}%
\fontfamily{#3}\fontseries{#4}\fontshape{#5}%
\selectfont}%
\fi\endgroup%
\begin{picture}(12534,8879)(439,-8907)
\thinlines
{\color[rgb]{0,0,0}\put(2458,-5596){\vector( 0,-1){630}}
}%
{\color[rgb]{0,0,0}\put(2458,-4799){\vector( 0,-1){270}}
}%
{\color[rgb]{0,0,0}\put(2458,-4269){\line( 0,-1){260}}
}%
{\color[rgb]{0,0,0}\put(2458,-3645){\vector( 0,-1){270}}
}%
{\color[rgb]{0,0,0}\put(2458,-3115){\line( 0,-1){260}}
}%
{\color[rgb]{0,0,0}\put(2458,-2491){\vector( 0,-1){270}}
}%
{\color[rgb]{0,0,0}\put(2458,-1961){\line( 0,-1){260}}
}%
{\color[rgb]{0,0,0}\put(10773,-5551){\vector( 0,-1){900}}
}%
{\color[rgb]{0,0,0}\put(10773,-4799){\vector( 0,-1){270}}
}%
{\color[rgb]{0,0,0}\put(10773,-4269){\line( 0,-1){260}}
}%
{\color[rgb]{0,0,0}\put(10773,-3645){\vector( 0,-1){270}}
}%
{\color[rgb]{0,0,0}\put(10773,-3115){\line( 0,-1){260}}
}%
{\color[rgb]{0,0,0}\put(10773,-2491){\vector( 0,-1){270}}
}%
{\color[rgb]{0,0,0}\put(10773,-1961){\line( 0,-1){260}}
}%
{\color[rgb]{0,0,0}\put(6436,-3391){\line(-2, 3){595.385}}
}%
{\color[rgb]{0,0,0}\put(6571,-3391){\line( 0, 1){1530}}
}%
{\color[rgb]{0,0,0}\put(6706,-3391){\line( 2, 3){595.385}}
}%
{\color[rgb]{0,0,0}\put(7039,-3523){\line( 3, 2){488.077}}
}%
{\color[rgb]{0,0,0}\put(6226,-3548){\line(-3, 2){488.077}}
}%
{\color[rgb]{0,0,0}\put(5791,-4046){\line( 3, 2){405}}
}%
{\color[rgb]{0,0,0}\put(7253,-4056){\line(-3, 2){405}}
}%
{\color[rgb]{0,0,0}\put(6795,-4557){\line( 5, 2){411.207}}
}%
{\color[rgb]{0,0,0}\put(6283,-4558){\line(-5, 2){411.207}}
}%
{\color[rgb]{0,0,0}\put(5691,-5146){\line( 3, 2){405}}
}%
{\color[rgb]{0,0,0}\put(7403,-5146){\line(-3, 2){405}}
}%
{\color[rgb]{0,0,0}\put(6571,-5056){\line( 0, 1){180}}
}%
{\color[rgb]{0,0,0}\put(10773,-2755){\oval(3785,5632)}
%\put(9106,-164){\oval(210,210)[tl]}
%\put(12541,-5446){\oval(210,210)[br]}
%\put(12541,-164){\oval(210,210)[tr]}
%\put(9106,-5551){\line( 1, 0){3435}}
%\put(9106,-59){\line( 1, 0){3435}}
%\put(9001,-5446){\line( 0, 1){5282}}
%\put(12646,-5446){\line( 0, 1){5282}}
}%
{\color[rgb]{0,0,0}\put(2458,-2755){\oval(3785,5632)}
%{\color[rgb]{0,0,0}\put(781,-5491){\oval(210,210)[bl]}
%\put(781,-145){\oval(210,210)[tl]}
%\put(4306,-5491){\oval(210,210)[br]}
%\put(4306,-145){\oval(210,210)[tr]}
%\put(781,-5596){\line( 1, 0){3525}}
%\put(781,-40){\line( 1, 0){3525}}
%\put(676,-5491){\line( 0, 1){5346}}
%\put(4411,-5491){\line( 0, 1){5346}}
}%
{\color[rgb]{0,0,0}\put(6623,-2755){\oval(3785,5632)}
%{\color[rgb]{0,0,0}\put(4966,-5491){\oval(210,210)[bl]}
%\put(4966,-166){\oval(210,210)[tl]}
%\put(8430,-5491){\oval(210,210)[br]}
%\put(8430,-166){\oval(210,210)[tr]}
%\put(4966,-5596){\line( 1, 0){3464}}
%\put(4966,-61){\line( 1, 0){3464}}
%\put(4861,-5491){\line( 0, 1){5325}}
%\put(8535,-5491){\line( 0, 1){5325}}
}%
{\color[rgb]{0,0,0}\put(4361,-2851){\line( 1, 0){350}}
}%
{\color[rgb]{0,0,0}\put(8521,-2851){\vector( 1, 0){350}}
}%
{\color[rgb]{0,0,0}\put(751,-7276){\oval(330,330)[bl]}
\put(751,-6526){\oval(330,330)[tl]}
\put(2941,-7276){\oval(330,330)[br]}
\put(2941,-6526){\oval(330,330)[tr]}
\put(751,-7441){\line( 1, 0){2190}}
\put(751,-6361){\line( 1, 0){2190}}
\put(586,-7276){\line( 0, 1){750}}
\put(3106,-7276){\line( 0, 1){750}}
}%
{\color[rgb]{0,0,0}\put(586,-8760){\oval(270,270)[bl]}
\put(586,-6361){\oval(270,270)[tl]}
\put(5851,-8760){\oval(270,270)[br]}
\put(5851,-6361){\oval(270,270)[tr]}
\put(586,-8895){\line( 1, 0){5265}}
\put(586,-6226){\line( 1, 0){5265}}
\put(451,-8760){\line( 0, 1){2399}}
\put(5986,-8760){\line( 0, 1){2399}}
}%
{\color[rgb]{0,0,0}\put(1726,-8551){\oval(300,300)[bl]}
\put(1726,-7906){\oval(300,300)[tl]}
\put(4411,-8551){\oval(300,300)[br]}
\put(4411,-7906){\oval(300,300)[tr]}
\put(1726,-8701){\line( 1, 0){2685}}
\put(1726,-7756){\line( 1, 0){2685}}
\put(1576,-8551){\line( 0, 1){645}}
\put(4561,-8551){\line( 0, 1){645}}
}%
{\color[rgb]{0,0,0}\put(8537,-8101){\oval(300,300)[bl]}
\put(8537,-6646){\oval(300,300)[tl]}
\put(12811,-8101){\oval(300,300)[br]}
\put(12811,-6646){\oval(300,300)[tr]}
\put(8537,-8251){\line( 1, 0){4274}}
\put(8537,-6496){\line( 1, 0){4274}}
\put(8387,-8101){\line( 0, 1){1455}}
\put(12961,-8101){\line( 0, 1){1455}}
}%
{\color[rgb]{0,0,0}\put(3481,-7290){\oval(300,300)[bl]}
\put(3481,-6531){\oval(300,300)[tl]}
\put(5656,-7290){\oval(300,300)[br]}
\put(5656,-6531){\oval(300,300)[tr]}
\put(3481,-7440){\line( 1, 0){2175}}
\put(3481,-6381){\line( 1, 0){2175}}
\put(3331,-7290){\line( 0, 1){759}}
\put(5806,-7290){\line( 0, 1){759}}
}%
{\color[rgb]{0,0,0}\put(5986,-7441){\vector( 1, 0){2385}}
}%
\put(2135,-1861){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Text}%
}}}
\put(2106,-2438){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}\emph{Parser}}%
}}}
\put(1441,-3015){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Abstract syntax}%
}}}
\put(1616,-3592){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}\emph{Static analysis}}%
}}}
\put(1131,-4169){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}(Signature, Sentences)}%
}}}
\put(1896,-4746){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}\emph{Interfaces}}%
}}}
\put(1641,-5323){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}XML, ATerms}%
}}}
\put(6301,-3706){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}CASL}%
}}}
\put(5356,-2356){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}CoCASL}%
}}}
\put(6976,-2356){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}CASL-LTL}%
}}}
\put(6121,-1726){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}CSP-CASL}%
}}}
\put(7201,-3121){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}SB-CASL}%
}}}
\put(5041,-3166){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}HasCASL}%
}}}
\put(5086,-4336){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}SubFOL$^=$}%
}}}
\put(7246,-4336){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}PFOL$^=$}%
}}}
\put(6346,-4786){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}FOL$^=$}%
}}}
\put(6346,-5371){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Horn$^=$}%
}}}
\put(5400,-5371){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\bullet$}%
}}}
\put(7600,-5371){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}$\bullet$}%
}}}
\put(1006,-421){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}Basic specifications}%
}}}
\put(826,-826){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}(logic-specific tools for}%
}}}
\put(826,-1231){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}CASL and extensions)}%
}}}
\put(5411,-421){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}Graph of CASL}%
}}}
\put(9591,-421){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}Structured and}%
}}}
\put(9771,-826){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}architectural}%
}}}
\put(9796,-1231){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}specifications}%
}}}
\put(10501,-1861){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Text}%
}}}
\put(10441,-2428){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}\emph{Parser}}%
}}}
\put(9886,-3015){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Abstract syntax}%
}}}
\put(9936,-3592){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}\emph{Static analysis}}%
}}}
\put(9641,-4169){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Development graph}%
}}}
\put(10216,-4746){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}\emph{Interfaces}}%
}}}
\put(9946,-5323){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}XML, ATerms}%
}}}
\put(2476,-8476){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}(e.g. CCC)}%
}}}
\put(1936,-8161){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Consistency checker}%
}}}
\put(846,-7171){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}(e.g. HOL-CASL)}%
}}}
\put(936,-6766){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Theorem prover}%
}}}
\put(8806,-7846){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Management of proofs \& change}%
}}}
\put(9091,-7351){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Heterogeneous proof engine}%
}}}
\put(10206,-6946){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}MAYA}%
}}}
\put(3501,-7216){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}(e.g. ELAN-CASL)}%
}}}
\put(4051,-6766){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}{\color[rgb]{0,0,0}Rewriter}%
}}}
\put(5106,-1231){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}proposed extensions}%
}}}
\put(5280,-826){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\bfdefault}{\updefault}{\color[rgb]{0,0,0}sublanguages and}%
}}}
\end{picture}