2 %%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005)
3 %%For: (sacerdot) Claudio Sacerdoti Coen,,,
6 %%BoundingBox: 35 35 1070 1263
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 1070 1263
234 %%PageOrientation: Portrait
236 35 35 1035 1228 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 596 778 moveto
253 0.000 0.000 1.000 sethsbcolor
254 newpath 596 778 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 68 814 moveto
279 0.000 0.000 1.000 sethsbcolor
280 newpath 68 814 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 289 296 moveto
305 0.000 0.000 1.000 sethsbcolor
306 newpath 289 296 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 559 16 moveto
331 0.000 0.000 1.000 sethsbcolor
332 newpath 559 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 714 848 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 352 636 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 681 825 moveto
373 658 810 625 790 594 778 curveto
374 581 772 574 779 562 770 curveto
375 538 749 557 725 533 704 curveto
376 493 667 467 688 416 668 curveto
377 410 665 403 663 397 660 curveto
382 0.000 0.000 0.000 edgecolor
383 newpath 398 657 moveto
388 0.000 0.000 0.000 edgecolor
389 newpath 398 657 moveto
398 714 936 109 25 ellipse_path
403 [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]
408 % cic_disambiguation -> acic_content
409 newpath 714 910 moveto
410 714 902 714 893 714 884 curveto
415 0.000 0.000 0.000 edgecolor
416 newpath 718 884 moveto
421 0.000 0.000 0.000 edgecolor
422 newpath 718 884 moveto
431 359 848 86 25 ellipse_path
436 [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]
441 % cic_disambiguation -> cic_unification
442 newpath 639 917 moveto
443 579 903 495 882 435 867 curveto
448 0.000 0.000 0.000 edgecolor
449 newpath 435 864 moveto
454 0.000 0.000 0.000 edgecolor
455 newpath 435 864 moveto
464 479 736 44 25 ellipse_path
469 [17.28 12 10.56 6.72 12]
474 % cic_disambiguation -> whelp
475 newpath 679 912 moveto
476 664 900 645 887 629 874 curveto
477 586 838 538 794 509 765 curveto
482 0.000 0.000 0.000 edgecolor
483 newpath 512 763 moveto
488 0.000 0.000 0.000 edgecolor
489 newpath 512 763 moveto
498 919 936 76 25 ellipse_path
503 [10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36]
508 % content_pres -> acic_content
509 newpath 872 916 moveto
510 841 903 802 886 770 872 curveto
515 0.000 0.000 0.000 edgecolor
516 newpath 772 869 moveto
521 0.000 0.000 0.000 edgecolor
522 newpath 772 869 moveto
531 873 366 75 25 ellipse_path
536 [12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36]
541 % content_pres -> utf8_macros
542 newpath 916 910 moveto
543 911 872 903 799 903 736 curveto
544 903 736 903 736 903 542 curveto
545 903 492 891 437 883 402 curveto
550 0.000 0.000 0.000 edgecolor
551 newpath 886 401 moveto
556 0.000 0.000 0.000 edgecolor
557 newpath 886 401 moveto
566 686 1128 81 25 ellipse_path
571 [12 7.92 10.56 7.92 6.72 6.72 10.56 12 12 10.56 7.92 9.36 10.56 7.92]
578 714 1024 50 25 ellipse_path
583 [6.72 10.56 12 6.72 10.56 12 12]
588 % grafite_parser -> lexicon
589 newpath 693 1103 moveto
590 696 1090 701 1074 705 1059 curveto
595 0.000 0.000 0.000 edgecolor
596 newpath 708 1059 moveto
601 0.000 0.000 0.000 edgecolor
602 newpath 708 1059 moveto
611 161 936 46 25 ellipse_path
616 [12 7.92 10.56 7.92 6.72 6.72 10.56]
621 % grafite_parser -> grafite
622 newpath 632 1109 moveto
623 623 1106 613 1104 604 1102 curveto
624 591 1099 495 1102 484 1094 curveto
625 450 1066 489 1027 455 998 curveto
626 389 938 345 981 258 962 curveto
627 243 959 227 955 213 951 curveto
632 0.000 0.000 0.000 edgecolor
633 newpath 214 948 moveto
638 0.000 0.000 0.000 edgecolor
639 newpath 214 948 moveto
646 % lexicon -> cic_disambiguation
647 newpath 714 998 moveto
648 714 990 714 981 714 972 curveto
653 0.000 0.000 0.000 edgecolor
654 newpath 718 972 moveto
659 0.000 0.000 0.000 edgecolor
660 newpath 718 972 moveto
667 % lexicon -> content_pres
668 newpath 753 1007 moveto
669 784 994 828 976 862 960 curveto
674 0.000 0.000 0.000 edgecolor
675 newpath 864 963 moveto
680 0.000 0.000 0.000 edgecolor
681 newpath 864 963 moveto
690 359 736 46 25 ellipse_path
695 [6.72 6.72 12 7.92 10.56 7.92 12]
700 % cic_unification -> library
701 newpath 359 822 moveto
702 359 807 359 788 359 772 curveto
707 0.000 0.000 0.000 edgecolor
708 newpath 363 772 moveto
713 0.000 0.000 0.000 edgecolor
714 newpath 363 772 moveto
723 313 936 45 25 ellipse_path
728 [6.72 10.56 10.56 6.72 6.72 10.56 9.36]
733 % tactics -> cic_unification
734 newpath 326 911 moveto
735 331 902 336 892 340 882 curveto
740 0.000 0.000 0.000 edgecolor
741 newpath 343 883 moveto
746 0.000 0.000 0.000 edgecolor
747 newpath 343 883 moveto
755 newpath 289 914 moveto
756 279 903 268 889 263 874 curveto
757 249 833 234 808 263 778 curveto
758 275 765 399 774 415 770 curveto
759 424 768 432 764 440 760 curveto
764 0.000 0.000 0.000 edgecolor
765 newpath 442 763 moveto
770 0.000 0.000 0.000 edgecolor
771 newpath 442 763 moveto
780 355 1024 90 25 ellipse_path
785 [12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12]
790 % paramodulation -> tactics
791 newpath 343 999 moveto
792 338 990 333 980 329 970 curveto
797 0.000 0.000 0.000 edgecolor
798 newpath 332 969 moveto
803 0.000 0.000 0.000 edgecolor
804 newpath 332 969 moveto
813 408 454 28 25 ellipse_path
824 newpath 160 910 moveto
825 158 872 155 798 155 736 curveto
826 155 736 155 736 155 636 curveto
827 155 556 219 554 288 516 curveto
828 327 495 343 502 379 480 curveto
829 379 480 380 480 380 479 curveto
834 0.000 0.000 0.000 edgecolor
835 newpath 382 482 moveto
840 0.000 0.000 0.000 edgecolor
841 newpath 382 482 moveto
850 161 1024 84 25 ellipse_path
855 [12 7.92 10.56 7.92 6.72 6.72 10.56 12 10.56 12 12 6.72 12 10.56]
860 % grafite_engine -> tactics
861 newpath 200 1001 moveto
862 222 989 249 973 272 960 curveto
867 0.000 0.000 0.000 edgecolor
868 newpath 274 963 moveto
873 0.000 0.000 0.000 edgecolor
874 newpath 274 963 moveto
881 % grafite_engine -> grafite
882 newpath 161 998 moveto
883 161 990 161 981 161 972 curveto
888 0.000 0.000 0.000 edgecolor
889 newpath 165 972 moveto
894 0.000 0.000 0.000 edgecolor
895 newpath 165 972 moveto
904 424 366 70 25 ellipse_path
909 [12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92]
915 newpath 413 429 moveto
916 414 420 416 411 417 402 curveto
921 0.000 0.000 0.000 edgecolor
922 newpath 420 402 moveto
927 0.000 0.000 0.000 edgecolor
928 newpath 420 402 moveto
937 622 174 33 25 ellipse_path
948 newpath 383 440 moveto
949 369 431 352 417 344 400 curveto
950 325 358 319 334 344 296 curveto
951 396 216 514 188 578 178 curveto
956 0.000 0.000 0.000 edgecolor
957 newpath 578 181 moveto
962 0.000 0.000 0.000 edgecolor
963 newpath 578 181 moveto
972 408 542 110 25 ellipse_path
977 [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]
982 % cic_proof_checking -> cic
983 newpath 408 516 moveto
984 408 508 408 499 408 490 curveto
989 0.000 0.000 0.000 edgecolor
990 newpath 412 490 moveto
995 0.000 0.000 0.000 edgecolor
996 newpath 412 490 moveto
1005 500 454 42 25 ellipse_path
1010 [12 10.56 6.72 6.72 10.56 7.92]
1015 % cic_proof_checking -> getter
1016 newpath 418 516 moveto
1017 430 501 446 487 460 477 curveto
1022 0.000 0.000 0.000 edgecolor
1023 newpath 462 480 moveto
1028 0.000 0.000 0.000 edgecolor
1029 newpath 462 480 moveto
1036 % getter -> urimanager
1037 newpath 480 431 moveto
1038 472 421 461 409 452 398 curveto
1043 0.000 0.000 0.000 edgecolor
1044 newpath 455 396 moveto
1049 0.000 0.000 0.000 edgecolor
1050 newpath 455 396 moveto
1059 748 262 52 25 ellipse_path
1064 [7.92 10.56 12 6.72 9.36 6.72 7.92 12]
1069 % getter -> registry
1070 newpath 501 428 moveto
1071 505 392 517 327 558 296 curveto
1072 570 287 673 291 686 288 curveto
1073 691 287 696 285 700 284 curveto
1078 0.000 0.000 0.000 edgecolor
1079 newpath 702 287 moveto
1084 0.000 0.000 0.000 edgecolor
1085 newpath 702 287 moveto
1094 613 366 45 25 ellipse_path
1099 [6.72 12 12 12 10.56 7.92]
1105 newpath 526 434 moveto
1106 541 422 561 406 578 393 curveto
1111 0.000 0.000 0.000 edgecolor
1112 newpath 580 396 moveto
1117 0.000 0.000 0.000 edgecolor
1118 newpath 580 396 moveto
1127 484 636 58 25 ellipse_path
1132 [18.72 10.56 6.72 10.56 12 10.56 6.72 10.56]
1138 newpath 505 612 moveto
1139 525 586 548 546 528 516 curveto
1140 507 483 483 498 448 480 curveto
1141 445 478 443 477 440 475 curveto
1146 0.000 0.000 0.000 edgecolor
1147 newpath 441 472 moveto
1152 0.000 0.000 0.000 edgecolor
1153 newpath 441 472 moveto
1162 728 366 50 25 ellipse_path
1167 [12 18.72 12 9.36 12 6.72]
1172 % metadata -> hmysql
1173 newpath 539 626 moveto
1174 600 616 638 623 686 568 curveto
1175 727 521 731 446 730 402 curveto
1180 0.000 0.000 0.000 edgecolor
1181 newpath 734 402 moveto
1186 0.000 0.000 0.000 edgecolor
1187 newpath 734 402 moveto
1195 newpath 480 711 moveto
1196 481 699 482 685 482 672 curveto
1201 0.000 0.000 0.000 edgecolor
1202 newpath 485 672 moveto
1207 0.000 0.000 0.000 edgecolor
1208 newpath 485 672 moveto
1215 % library -> metadata
1216 newpath 386 715 moveto
1217 404 700 428 680 448 664 curveto
1222 0.000 0.000 0.000 edgecolor
1223 newpath 450 667 moveto
1228 0.000 0.000 0.000 edgecolor
1229 newpath 450 667 moveto
1236 % library -> cic_acic
1237 newpath 357 711 moveto
1238 356 699 355 685 355 672 curveto
1243 0.000 0.000 0.000 edgecolor
1244 newpath 358 672 moveto
1249 0.000 0.000 0.000 edgecolor
1250 newpath 358 672 moveto
1257 % cic_acic -> cic_proof_checking
1258 newpath 367 611 moveto
1259 373 600 381 587 388 576 curveto
1264 0.000 0.000 0.000 edgecolor
1265 newpath 391 577 moveto
1270 0.000 0.000 0.000 edgecolor
1271 newpath 391 577 moveto
1280 622 86 42 25 ellipse_path
1285 [10.56 12 6.72 6.72 6.72 12]
1292 622 262 54 25 ellipse_path
1297 [12 12 12 12 18.72 10.56]
1303 newpath 622 236 moveto
1304 622 228 622 219 622 210 curveto
1309 0.000 0.000 0.000 edgecolor
1310 newpath 626 210 moveto
1315 0.000 0.000 0.000 edgecolor
1316 newpath 626 210 moveto
1323 % hmysql -> registry
1324 newpath 733 341 moveto
1325 735 328 738 312 741 298 curveto
1330 0.000 0.000 0.000 edgecolor
1331 newpath 744 298 moveto
1336 0.000 0.000 0.000 edgecolor
1337 newpath 744 298 moveto
1345 newpath 718 241 moveto
1346 699 228 674 211 655 197 curveto
1351 0.000 0.000 0.000 edgecolor
1352 newpath 657 194 moveto
1357 0.000 0.000 0.000 edgecolor
1358 newpath 657 194 moveto
1366 newpath 622 148 moveto
1367 622 140 622 131 622 122 curveto
1372 0.000 0.000 0.000 edgecolor
1373 newpath 626 122 moveto
1378 0.000 0.000 0.000 edgecolor
1379 newpath 626 122 moveto
1386 % DependencyAnalyzer
1389 0.584 0.220 0.933 nodecolor
1390 0.584 0.220 0.933 nodecolor
1391 newpath 716 768 moveto
1397 0.584 0.220 0.933 nodecolor
1398 newpath 716 768 moveto
1405 0.000 0.000 0.000 nodecolor
1408 [17.28 10.56 12 10.56 12 12 10.56 12 10.56 12]
1412 [17.28 12 10.56 6.72 12 10.56 10.56 7.92]
1417 % DependencyAnalyzer -> metadata
1418 newpath 595 704 moveto
1419 573 691 547 675 527 662 curveto
1424 0.000 0.000 0.000 edgecolor
1425 newpath 528 659 moveto
1430 0.000 0.000 0.000 edgecolor
1431 newpath 528 659 moveto
1441 0.584 0.220 0.933 nodecolor
1442 0.584 0.220 0.933 nodecolor
1443 newpath 635 560 moveto
1449 0.584 0.220 0.933 nodecolor
1450 newpath 635 560 moveto
1457 0.000 0.000 0.000 nodecolor
1460 [17.28 10.56 6.72 6.72 10.56 7.92]
1466 newpath 577 524 moveto
1467 563 512 546 496 532 483 curveto
1472 0.000 0.000 0.000 edgecolor
1473 newpath 534 480 moveto
1478 0.000 0.000 0.000 edgecolor
1479 newpath 534 480 moveto
1489 0.584 0.220 0.933 nodecolor
1490 0.584 0.220 0.933 nodecolor
1491 newpath 200 1226 moveto
1497 0.584 0.220 0.933 nodecolor
1498 newpath 200 1226 moveto
1505 0.000 0.000 0.000 nodecolor
1508 [21.36 10.56 6.72 6.72 6.72 10.56]
1513 % Matita -> grafite_parser
1514 newpath 200 1205 moveto
1515 294 1199 529 1181 604 1162 curveto
1516 613 1160 622 1157 631 1153 curveto
1521 0.000 0.000 0.000 edgecolor
1522 newpath 632 1156 moveto
1527 0.000 0.000 0.000 edgecolor
1528 newpath 632 1156 moveto
1535 % Matita -> grafite_engine
1536 newpath 161 1190 moveto
1537 161 1160 161 1099 161 1060 curveto
1542 0.000 0.000 0.000 edgecolor
1543 newpath 165 1060 moveto
1548 0.000 0.000 0.000 edgecolor
1549 newpath 165 1060 moveto
1557 newpath 141 1190 moveto
1558 118 1169 83 1132 64 1094 curveto
1559 50 1065 48 1055 48 1024 curveto
1560 48 1024 48 1024 48 454 curveto
1561 48 327 166 338 285 296 curveto
1562 334 278 473 269 557 265 curveto
1567 0.000 0.000 0.000 edgecolor
1568 newpath 557 268 moveto
1573 0.000 0.000 0.000 edgecolor
1574 newpath 557 268 moveto
1584 0.584 0.220 0.933 nodecolor
1585 0.584 0.220 0.933 nodecolor
1586 newpath 279 668 moveto
1592 0.584 0.220 0.933 nodecolor
1593 newpath 279 668 moveto
1600 0.000 0.000 0.000 nodecolor
1603 [13.44 7.92 12 12 7.92]
1607 [16.08 12 10.56 10.56 12 10.56 7.92]
1612 % ProofChecker -> cic_proof_checking
1613 newpath 279 607 moveto
1614 281 606 283 605 285 604 curveto
1615 306 592 330 580 351 569 curveto
1620 0.000 0.000 0.000 edgecolor
1621 newpath 352 572 moveto
1626 0.000 0.000 0.000 edgecolor
1627 newpath 352 572 moveto
1637 0.584 0.220 0.933 nodecolor
1638 0.584 0.220 0.933 nodecolor
1639 newpath 588 1042 moveto
1645 0.584 0.220 0.933 nodecolor
1646 newpath 588 1042 moveto
1653 0.000 0.000 0.000 nodecolor
1656 [17.28 17.28 12 12 12]
1661 % Uwobo -> content_pres
1662 newpath 574 1006 moveto
1663 580 1003 586 1000 592 998 curveto
1664 695 963 728 985 833 962 curveto
1665 840 961 846 959 853 957 curveto
1670 0.000 0.000 0.000 edgecolor
1671 newpath 854 960 moveto
1676 0.000 0.000 0.000 edgecolor
1677 newpath 854 960 moveto
1687 0.584 0.220 0.933 nodecolor
1688 0.584 0.220 0.933 nodecolor
1689 newpath 726 1226 moveto
1695 0.584 0.220 0.933 nodecolor
1696 newpath 726 1226 moveto
1703 0.000 0.000 0.000 nodecolor
1706 [22.56 12 10.56 6.72 12]
1711 % Whelp -> grafite_parser
1712 newpath 686 1190 moveto
1713 686 1182 686 1173 686 1164 curveto
1718 0.000 0.000 0.000 edgecolor
1719 newpath 690 1164 moveto
1724 0.000 0.000 0.000 edgecolor
1725 newpath 690 1164 moveto