2 %%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005)
3 %%For: (zacchiro) Stefano Zacchiroli,,,
6 %%BoundingBox: 35 35 1332 937
15 /EncodingVector 256 array def
18 ISOLatin1Encoding 0 255 getinterval putinterval
71 % Set up ISO Latin 1 character encoding
73 dup dup findfont dup length dict begin
74 { 1 index /FID ne { def }{ pop pop } ifelse
76 /Encoding EncodingVector def
77 currentdict end definefont
79 /Times-Roman starnetISO def
80 /Times-Italic starnetISO def
81 /Times-Bold starnetISO def
82 /Times-BoldItalic starnetISO def
83 /Helvetica starnetISO def
84 /Helvetica-Oblique starnetISO def
85 /Helvetica-Bold starnetISO def
86 /Helvetica-BoldOblique starnetISO def
87 /Courier starnetISO def
88 /Courier-Oblique starnetISO def
89 /Courier-Bold starnetISO def
90 /Courier-BoldOblique starnetISO def
94 %%BeginResource: procset graphviz 0 0
95 /coord-font-family /Times-Roman def
96 /default-font-family /Times-Roman def
97 /coordfont coord-font-family findfont 8 scalefont def
99 /InvScaleFactor 1.0 def
101 dup 1 exch div /InvScaleFactor exch def
106 /solid { [] 0 setdash } bind def
107 /dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
108 /dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
109 /invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
110 /bold { 2 setlinewidth } bind def
112 /unfilled { } bind def
113 /rounded { } bind def
114 /diagonals { } bind def
116 % hooks for setting color
117 /nodecolor { sethsbcolor } bind def
118 /edgecolor { sethsbcolor } bind def
119 /graphcolor { sethsbcolor } bind def
120 /nopcolor {pop pop pop} bind def
122 /beginpage { % i j npages
131 (\() show i str cvs show (,) show j str cvs show (\)) show
141 % draw aligned label in bounding box aligned to current point
142 /alignedtext { % width adj text
148 text stringwidth pop adj mul 0 rmoveto
155 /boxprim { % xcorner ycorner xsize ysize
178 /endpage { showpage } bind def
182 [ % layer color sequence - darkest to lightest
191 /layerlen layercolorseq length def
193 /setlayer {/maxlayer exch def /curlayer exch def
194 layercolorseq curlayer 1 sub layerlen mod get
195 aload pop sethsbcolor
196 /nodecolor {nopcolor} def
197 /edgecolor {nopcolor} def
198 /graphcolor {nopcolor} def
201 /onlayer { curlayer ne {invis} if } def
217 14 default-font-family set_font
219 % /arrowlength 10 def
222 % make sure pdfmark is harmless for PS-interpreters other than Distiller
223 /pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
224 % make '<<' and '>>' safe on PS Level 1 devices
225 /languagelevel where {pop languagelevel}{1} ifelse
227 userdict (<<) cvn ([) cvn load put
228 userdict (>>) cvn ([) cvn load put
233 %%PageBoundingBox: 36 36 1332 937
234 %%PageOrientation: Portrait
236 35 35 1297 902 boxprim clip newpath
239 0 0 translate 0 rotate
240 0.000 0.000 0.000 graphcolor
241 24.00 /Times-Roman set_font
242 % cluster_presentation
245 0.000 0.000 1.000 sethsbcolor
246 0.000 0.000 0.929 sethsbcolor
247 newpath 772 488 moveto
253 0.000 0.000 1.000 sethsbcolor
254 newpath 772 488 moveto
261 0.000 0.000 0.000 sethsbcolor
263 (Terms at the content and presentation level)
264 [14.64 10.56 7.92 18.72 9.36 6 10.56 6.72 6 6.72 12 10.56 6 10.56 12 12 6.72 10.56 12 6.72 6 10.56 12 12 6 12 7.92 10.56 9.36 10.56 12 6.72 10.56 6.72 6.72 12 12 6 6.72 10.56 12 10.56 6.72]
271 0.000 0.000 1.000 sethsbcolor
272 0.000 0.000 0.929 sethsbcolor
273 newpath 330 612 moveto
279 0.000 0.000 1.000 sethsbcolor
280 newpath 330 612 moveto
287 0.000 0.000 0.000 sethsbcolor
289 (Partially specified terms)
290 [13.44 10.56 7.92 6.72 6.72 10.56 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36]
297 0.000 0.000 1.000 sethsbcolor
298 0.000 0.000 0.929 sethsbcolor
299 newpath 232 208 moveto
305 0.000 0.000 1.000 sethsbcolor
306 newpath 232 208 moveto
313 0.000 0.000 0.000 sethsbcolor
315 (Fully specified terms)
316 [13.44 12 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36]
323 0.000 0.000 1.000 sethsbcolor
324 0.000 0.000 0.929 sethsbcolor
325 newpath 614 16 moveto
331 0.000 0.000 1.000 sethsbcolor
332 newpath 614 16 moveto
339 0.000 0.000 0.000 sethsbcolor
342 [17.28 6.72 6.72 6.72 6.72 6.72 6.72 10.56 9.36]
349 915 646 75 25 ellipse_path
354 [10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72]
361 876 558 54 25 ellipse_path
366 [10.56 6.72 10.56 12 10.56 10.56 6.72 10.56]
371 % acic_content -> cic_acic
372 newpath 904 621 moveto
373 900 612 895 602 891 592 curveto
378 0.000 0.000 0.000 edgecolor
379 newpath 894 591 moveto
384 0.000 0.000 0.000 edgecolor
385 newpath 894 591 moveto
394 487 454 110 25 ellipse_path
399 [10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12]
404 % cic_acic -> cic_proof_checking
405 newpath 863 533 moveto
406 854 517 840 498 821 488 curveto
407 803 477 693 468 604 462 curveto
412 0.000 0.000 0.000 edgecolor
413 newpath 604 459 moveto
418 0.000 0.000 0.000 edgecolor
419 newpath 604 459 moveto
428 890 734 109 25 ellipse_path
433 [10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12]
438 % cic_disambiguation -> acic_content
439 newpath 897 709 moveto
440 900 700 903 691 905 682 curveto
445 0.000 0.000 0.000 edgecolor
446 newpath 908 683 moveto
451 0.000 0.000 0.000 edgecolor
452 newpath 908 683 moveto
461 485 646 86 25 ellipse_path
466 [10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12]
471 % cic_disambiguation -> cic_unification
472 newpath 810 717 moveto
473 738 702 636 679 565 663 curveto
478 0.000 0.000 0.000 edgecolor
479 newpath 565 660 moveto
484 0.000 0.000 0.000 edgecolor
485 newpath 565 660 moveto
494 336 558 44 25 ellipse_path
499 [17.28 12 10.56 6.72 12]
504 % cic_disambiguation -> whelp
505 newpath 845 711 moveto
506 786 682 680 634 584 612 curveto
507 535 600 397 620 354 592 curveto
508 354 592 353 592 353 591 curveto
513 0.000 0.000 0.000 edgecolor
514 newpath 356 589 moveto
519 0.000 0.000 0.000 edgecolor
520 newpath 356 589 moveto
529 1095 734 76 25 ellipse_path
534 [10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36]
539 % content_pres -> acic_content
540 newpath 1051 713 moveto
541 1026 700 994 685 967 672 curveto
546 0.000 0.000 0.000 edgecolor
547 newpath 968 669 moveto
552 0.000 0.000 0.000 edgecolor
553 newpath 968 669 moveto
562 818 366 75 25 ellipse_path
567 [12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36]
572 % content_pres -> utf8_macros
573 newpath 1082 709 moveto
574 1057 662 1000 562 940 488 curveto
575 914 454 879 421 854 397 curveto
580 0.000 0.000 0.000 edgecolor
581 newpath 856 394 moveto
586 0.000 0.000 0.000 edgecolor
587 newpath 856 394 moveto
596 1095 822 46 25 ellipse_path
601 [12 7.92 10.56 7.92 6.72 6.72 10.56]
606 % grafite -> content_pres
607 newpath 1095 796 moveto
608 1095 788 1095 779 1095 770 curveto
613 0.000 0.000 0.000 edgecolor
614 newpath 1099 770 moveto
619 0.000 0.000 0.000 edgecolor
620 newpath 1099 770 moveto
627 % cic_unification -> cic_proof_checking
628 newpath 485 620 moveto
629 486 586 486 528 487 490 curveto
634 0.000 0.000 0.000 edgecolor
635 newpath 491 490 moveto
640 0.000 0.000 0.000 edgecolor
641 newpath 491 490 moveto
650 482 734 45 25 ellipse_path
655 [6.72 10.56 10.56 6.72 6.72 10.56 9.36]
660 % tactics -> cic_unification
661 newpath 483 708 moveto
662 483 700 484 691 484 682 curveto
667 0.000 0.000 0.000 edgecolor
668 newpath 488 682 moveto
673 0.000 0.000 0.000 edgecolor
674 newpath 488 682 moveto
682 newpath 451 715 moveto
683 428 701 399 682 389 672 curveto
684 370 648 356 617 347 593 curveto
689 0.000 0.000 0.000 edgecolor
690 newpath 350 591 moveto
695 0.000 0.000 0.000 edgecolor
696 newpath 350 591 moveto
705 479 822 90 25 ellipse_path
710 [12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12]
715 % paramodulation -> tactics
716 newpath 480 796 moveto
717 480 788 481 779 481 770 curveto
722 0.000 0.000 0.000 edgecolor
723 newpath 485 770 moveto
728 0.000 0.000 0.000 edgecolor
729 newpath 485 770 moveto
738 462 366 28 25 ellipse_path
750 494 278 70 25 ellipse_path
755 [12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92]
761 newpath 471 341 moveto
762 474 332 478 322 481 312 curveto
767 0.000 0.000 0.000 edgecolor
768 newpath 484 314 moveto
773 0.000 0.000 0.000 edgecolor
774 newpath 484 314 moveto
783 675 174 33 25 ellipse_path
794 newpath 442 347 moveto
795 432 336 420 320 414 304 curveto
796 401 263 386 240 414 208 curveto
797 428 192 560 181 631 177 curveto
802 0.000 0.000 0.000 edgecolor
803 newpath 631 180 moveto
808 0.000 0.000 0.000 edgecolor
809 newpath 631 180 moveto
816 % cic_proof_checking -> cic
817 newpath 480 429 moveto
818 477 420 474 410 472 401 curveto
823 0.000 0.000 0.000 edgecolor
824 newpath 475 400 moveto
829 0.000 0.000 0.000 edgecolor
830 newpath 475 400 moveto
839 323 366 42 25 ellipse_path
844 [12 10.56 6.72 6.72 10.56 7.92]
849 % cic_proof_checking -> getter
850 newpath 443 430 moveto
851 418 417 388 400 364 388 curveto
856 0.000 0.000 0.000 edgecolor
857 newpath 365 385 moveto
862 0.000 0.000 0.000 edgecolor
863 newpath 365 385 moveto
870 % getter -> urimanager
871 newpath 356 349 moveto
872 380 336 416 318 444 304 curveto
877 0.000 0.000 0.000 edgecolor
878 newpath 446 307 moveto
883 0.000 0.000 0.000 edgecolor
884 newpath 446 307 moveto
893 675 278 52 25 ellipse_path
898 [7.92 10.56 12 6.72 9.36 6.72 7.92 12]
904 newpath 362 355 moveto
905 381 350 404 345 424 340 curveto
906 507 321 530 327 610 304 curveto
907 615 302 621 300 626 298 curveto
912 0.000 0.000 0.000 edgecolor
913 newpath 627 301 moveto
918 0.000 0.000 0.000 edgecolor
919 newpath 627 301 moveto
928 299 454 58 25 ellipse_path
933 [18.72 10.56 6.72 10.56 12 10.56 6.72 10.56]
939 newpath 336 434 moveto
940 364 419 401 399 428 385 curveto
945 0.000 0.000 0.000 edgecolor
946 newpath 430 388 moveto
951 0.000 0.000 0.000 edgecolor
952 newpath 430 388 moveto
960 newpath 306 429 moveto
961 308 420 311 410 313 401 curveto
966 0.000 0.000 0.000 edgecolor
967 newpath 316 402 moveto
972 0.000 0.000 0.000 edgecolor
973 newpath 316 402 moveto
982 673 366 50 25 ellipse_path
987 [12 18.72 12 9.36 12 6.72]
993 newpath 341 436 moveto
994 349 433 358 430 367 428 curveto
995 473 402 507 432 610 400 curveto
996 618 398 625 394 632 391 curveto
1001 0.000 0.000 0.000 edgecolor
1002 newpath 634 394 moveto
1007 0.000 0.000 0.000 edgecolor
1008 newpath 634 394 moveto
1016 newpath 327 533 moveto
1017 322 520 316 503 311 488 curveto
1022 0.000 0.000 0.000 edgecolor
1023 newpath 314 487 moveto
1028 0.000 0.000 0.000 edgecolor
1029 newpath 314 487 moveto
1038 675 86 42 25 ellipse_path
1043 [10.56 12 6.72 6.72 6.72 12]
1050 801 278 54 25 ellipse_path
1055 [12 12 12 12 18.72 10.56]
1061 newpath 783 254 moveto
1062 771 239 754 221 737 208 curveto
1063 730 202 721 197 713 192 curveto
1068 0.000 0.000 0.000 edgecolor
1069 newpath 714 189 moveto
1074 0.000 0.000 0.000 edgecolor
1075 newpath 714 189 moveto
1082 % hmysql -> registry
1083 newpath 674 340 moveto
1084 674 332 674 323 674 314 curveto
1089 0.000 0.000 0.000 edgecolor
1090 newpath 678 314 moveto
1095 0.000 0.000 0.000 edgecolor
1096 newpath 678 314 moveto
1104 newpath 675 252 moveto
1105 675 239 675 224 675 210 curveto
1110 0.000 0.000 0.000 edgecolor
1111 newpath 679 210 moveto
1116 0.000 0.000 0.000 edgecolor
1117 newpath 679 210 moveto
1125 newpath 675 148 moveto
1126 675 140 675 131 675 122 curveto
1131 0.000 0.000 0.000 edgecolor
1132 newpath 679 122 moveto
1137 0.000 0.000 0.000 edgecolor
1138 newpath 679 122 moveto
1148 0.584 0.220 0.933 nodecolor
1149 0.584 0.220 0.933 nodecolor
1150 newpath 128 472 moveto
1156 0.584 0.220 0.933 nodecolor
1157 newpath 128 472 moveto
1164 0.000 0.000 0.000 nodecolor
1167 [17.28 7.92 10.56 17.28 17.28 7.92 10.56 12 12]
1172 % DrawGraph -> getter
1173 newpath 114 436 moveto
1174 122 433 130 430 137 428 curveto
1175 184 411 237 394 275 381 curveto
1180 0.000 0.000 0.000 edgecolor
1181 newpath 276 384 moveto
1186 0.000 0.000 0.000 edgecolor
1187 newpath 276 384 moveto
1197 0.584 0.220 0.933 nodecolor
1198 0.584 0.220 0.933 nodecolor
1199 newpath 222 472 moveto
1205 0.584 0.220 0.933 nodecolor
1206 newpath 222 472 moveto
1213 0.000 0.000 0.000 nodecolor
1216 [17.28 10.56 6.72 6.72 10.56 7.92]
1222 newpath 212 436 moveto
1223 233 423 262 405 285 390 curveto
1228 0.000 0.000 0.000 edgecolor
1229 newpath 286 393 moveto
1234 0.000 0.000 0.000 edgecolor
1235 newpath 286 393 moveto
1245 0.584 0.220 0.933 nodecolor
1246 0.584 0.220 0.933 nodecolor
1247 newpath 764 840 moveto
1253 0.584 0.220 0.933 nodecolor
1254 newpath 764 840 moveto
1261 0.000 0.000 0.000 nodecolor
1264 [21.36 10.56 6.72 6.72 6.72 10.56]
1269 % Matita -> cic_disambiguation
1270 newpath 754 804 moveto
1271 759 801 764 798 768 796 curveto
1272 789 784 813 772 833 762 curveto
1277 0.000 0.000 0.000 edgecolor
1278 newpath 835 765 moveto
1283 0.000 0.000 0.000 edgecolor
1284 newpath 835 765 moveto
1292 newpath 694 804 moveto
1293 689 801 683 798 677 796 curveto
1294 630 776 574 759 534 748 curveto
1299 0.000 0.000 0.000 edgecolor
1300 newpath 535 745 moveto
1305 0.000 0.000 0.000 edgecolor
1306 newpath 535 745 moveto
1316 0.584 0.220 0.933 nodecolor
1317 0.584 0.220 0.933 nodecolor
1318 newpath 764 576 moveto
1324 0.584 0.220 0.933 nodecolor
1325 newpath 764 576 moveto
1332 0.000 0.000 0.000 nodecolor
1335 [13.44 7.92 12 12 7.92 16.08 12 10.56 10.56 12 10.56 7.92]
1340 % ProofChecker -> cic_proof_checking
1341 newpath 673 540 moveto
1342 659 524 635 501 610 488 curveto
1343 601 483 590 478 580 474 curveto
1348 0.000 0.000 0.000 edgecolor
1349 newpath 581 471 moveto
1354 0.000 0.000 0.000 edgecolor
1355 newpath 581 471 moveto
1365 0.584 0.220 0.933 nodecolor
1366 0.584 0.220 0.933 nodecolor
1367 newpath 1295 840 moveto
1373 0.584 0.220 0.933 nodecolor
1374 newpath 1295 840 moveto
1381 0.000 0.000 0.000 nodecolor
1384 [17.28 17.28 12 12 12]
1389 % Uwobo -> acic_content
1390 newpath 1246 804 moveto
1391 1235 778 1214 732 1181 708 curveto
1392 1111 655 1074 662 999 653 curveto
1397 0.000 0.000 0.000 edgecolor
1398 newpath 999 650 moveto
1403 0.000 0.000 0.000 edgecolor
1404 newpath 999 650 moveto
1411 % Uwobo -> content_pres
1412 newpath 1221 804 moveto
1413 1216 801 1210 798 1205 796 curveto
1414 1165 778 1143 791 1113 767 curveto
1419 0.000 0.000 0.000 edgecolor
1420 newpath 1115 764 moveto
1425 0.000 0.000 0.000 edgecolor
1426 newpath 1115 764 moveto
1436 0.584 0.220 0.933 nodecolor
1437 0.584 0.220 0.933 nodecolor
1438 newpath 668 840 moveto
1444 0.584 0.220 0.933 nodecolor
1445 newpath 668 840 moveto
1452 0.000 0.000 0.000 nodecolor
1455 [22.56 12 10.56 6.72 12]
1460 % Whelp -> cic_disambiguation
1461 newpath 660 804 moveto
1462 666 801 671 798 677 796 curveto
1463 718 779 764 765 803 755 curveto
1468 0.000 0.000 0.000 edgecolor
1469 newpath 804 758 moveto
1474 0.000 0.000 0.000 edgecolor
1475 newpath 804 758 moveto
1483 newpath 602 804 moveto
1484 596 801 590 798 584 796 curveto
1485 530 776 365 803 326 760 curveto
1486 286 714 305 637 321 592 curveto
1491 0.000 0.000 0.000 edgecolor
1492 newpath 324 594 moveto
1497 0.000 0.000 0.000 edgecolor
1498 newpath 324 594 moveto