From 5aa0c59a1edd110c8207d74dede3a84fd500f418 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 25 Nov 2005 14:36:01 +0000 Subject: [PATCH] minor changes --- helm/papers/matita/libraries.dot | 6 +- helm/papers/matita/libraries.ps | 778 +++++++++++---------- helm/papers/matita/librariesCluster.ps | 921 ++++++++++++------------- helm/papers/matita/matita2.tex | 70 +- 4 files changed, 884 insertions(+), 891 deletions(-) diff --git a/helm/papers/matita/libraries.dot b/helm/papers/matita/libraries.dot index 2db2aa509..c4aedef50 100644 --- a/helm/papers/matita/libraries.dot +++ b/helm/papers/matita/libraries.dot @@ -49,7 +49,7 @@ digraph G { hgdome; hmysql; registry; - utf8_macros; +// utf8_macros; xml; } /* libs */ @@ -64,7 +64,7 @@ digraph G { metadata -> getter; metadata -> hmysql; grafite -> content_pres; - content_pres -> utf8_macros; +// content_pres -> utf8_macros; content_pres -> acic_content; acic_content -> cic_acic; cic_acic -> cic_proof_checking; @@ -94,7 +94,7 @@ digraph G { Getter -> getter; Matita -> cic_disambiguation; Matita -> grafite; -// Matita -> hgdome; + Matita -> hgdome; Matita -> paramodulation; ProofChecker -> cic_proof_checking; Uwobo -> content_pres; diff --git a/helm/papers/matita/libraries.ps b/helm/papers/matita/libraries.ps index aaf58d5ac..2ef6381e4 100644 --- a/helm/papers/matita/libraries.ps +++ b/helm/papers/matita/libraries.ps @@ -3,7 +3,7 @@ %%For: (zacchiro) Stefano Zacchiroli,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 778 885 +%%BoundingBox: 35 35 680 885 %%EndComments save %%BeginProlog @@ -230,10 +230,10 @@ def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 778 885 +%%PageBoundingBox: 36 36 680 885 %%PageOrientation: Portrait gsave -35 35 743 850 boxprim clip newpath +35 35 645 850 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0 0 translate 0 rotate @@ -242,10 +242,10 @@ gsave % acic_content gsave 10 dict begin -495 574 75 25 ellipse_path +497 574 75 25 ellipse_path stroke gsave 10 dict begin -434 566 moveto +436 566 moveto (acic_content) [10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72] xshow @@ -254,10 +254,10 @@ end grestore % cic_acic gsave 10 dict begin -464 480 54 25 ellipse_path +432 480 54 25 ellipse_path stroke gsave 10 dict begin -424 472 moveto +392 472 moveto (cic_acic) [10.56 6.72 10.56 12 10.56 10.56 6.72 10.56] xshow @@ -265,32 +265,32 @@ end grestore end grestore % acic_content -> cic_acic -newpath 487 548 moveto -483 538 479 526 475 515 curveto +newpath 480 549 moveto +472 538 463 525 455 513 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 478 514 moveto -472 505 lineto -472 516 lineto +newpath 457 510 moveto +449 504 lineto +452 514 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 478 514 moveto -472 505 lineto -472 516 lineto +newpath 457 510 moveto +449 504 lineto +452 514 lineto closepath stroke end grestore % cic_proof_checking gsave 10 dict begin -365 386 110 25 ellipse_path +441 386 110 25 ellipse_path stroke gsave 10 dict begin -269 378 moveto +345 378 moveto (cic_proof_checking) [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] xshow @@ -298,32 +298,32 @@ end grestore end grestore % cic_acic -> cic_proof_checking -newpath 440 457 moveto -427 445 412 431 399 418 curveto +newpath 434 454 moveto +435 444 436 433 437 422 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 401 415 moveto -391 411 lineto -396 420 lineto +newpath 440 422 moveto +438 412 lineto +434 422 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 401 415 moveto -391 411 lineto -396 420 lineto +newpath 440 422 moveto +438 412 lineto +434 422 lineto closepath stroke end grestore % cic_disambiguation gsave 10 dict begin -338 662 109 25 ellipse_path +318 662 109 25 ellipse_path stroke gsave 10 dict begin -243 654 moveto +223 654 moveto (cic_disambiguation) [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] xshow @@ -331,32 +331,32 @@ end grestore end grestore % cic_disambiguation -> acic_content -newpath 380 638 moveto -401 627 426 613 447 601 curveto +newpath 365 639 moveto +390 627 420 612 445 599 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 449 604 moveto -456 596 lineto -446 598 lineto +newpath 446 602 moveto +454 595 lineto +443 596 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 449 604 moveto -456 596 lineto -446 598 lineto +newpath 446 602 moveto +454 595 lineto +443 596 lineto closepath stroke end grestore % cic_unification gsave 10 dict begin -314 574 86 25 ellipse_path +316 574 86 25 ellipse_path stroke gsave 10 dict begin -242 566 moveto +244 566 moveto (cic_unification) [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] xshow @@ -364,22 +364,22 @@ end grestore end grestore % cic_disambiguation -> cic_unification -newpath 331 637 moveto -329 628 326 619 324 610 curveto +newpath 317 636 moveto +317 628 317 619 317 610 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 327 609 moveto -321 600 lineto -321 611 lineto +newpath 321 610 moveto +317 600 lineto +314 610 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 327 609 moveto -321 600 lineto -321 611 lineto +newpath 321 610 moveto +317 600 lineto +314 610 lineto closepath stroke end grestore @@ -397,32 +397,32 @@ end grestore end grestore % cic_disambiguation -> whelp -newpath 292 639 moveto -265 626 232 609 207 596 curveto +newpath 276 638 moveto +254 626 227 610 205 597 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 208 593 moveto -198 591 lineto -205 599 lineto +newpath 206 594 moveto +196 592 lineto +203 600 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 208 593 moveto -198 591 lineto -205 599 lineto +newpath 206 594 moveto +196 592 lineto +203 600 lineto closepath stroke end grestore % content_pres gsave 10 dict begin -543 662 76 25 ellipse_path +523 662 76 25 ellipse_path stroke gsave 10 dict begin -481 654 moveto +461 654 moveto (content_pres) [10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] xshow @@ -430,65 +430,32 @@ end grestore end grestore % content_pres -> acic_content -newpath 529 637 moveto -524 628 519 618 514 608 curveto +newpath 515 637 moveto +513 628 510 619 508 610 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 517 606 moveto -509 599 lineto -511 609 lineto +newpath 511 609 moveto +505 600 lineto +505 611 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 517 606 moveto -509 599 lineto -511 609 lineto -closepath -stroke -end grestore - -% utf8_macros -gsave 10 dict begin -665 574 75 25 ellipse_path -stroke -gsave 10 dict begin -604 566 moveto -(utf8_macros) -[12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36] -xshow -end grestore -end grestore - -% content_pres -> utf8_macros -newpath 575 639 moveto -590 628 609 615 625 603 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 627 606 moveto -633 597 lineto -623 600 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 627 606 moveto -633 597 lineto -623 600 lineto +newpath 511 609 moveto +505 600 lineto +505 611 lineto closepath stroke end grestore % grafite gsave 10 dict begin -601 750 46 25 ellipse_path +554 750 46 25 ellipse_path stroke gsave 10 dict begin -569 742 moveto +522 742 moveto (grafite) [12 7.92 10.56 7.92 6.72 6.72 10.56] xshow @@ -496,54 +463,54 @@ end grestore end grestore % grafite -> content_pres -newpath 585 726 moveto -579 717 571 706 565 696 curveto +newpath 545 725 moveto +542 716 539 706 535 697 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 567 693 moveto -559 687 lineto -562 697 lineto +newpath 538 696 moveto +532 687 lineto +532 698 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 567 693 moveto -559 687 lineto -562 697 lineto +newpath 538 696 moveto +532 687 lineto +532 698 lineto closepath stroke end grestore % cic_unification -> cic_proof_checking -newpath 329 549 moveto -335 538 342 524 346 512 curveto -356 482 360 447 362 422 curveto +newpath 323 549 moveto +330 522 345 479 368 448 curveto +376 437 387 426 397 417 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 365 422 moveto -363 412 lineto -359 422 lineto +newpath 400 419 moveto +405 410 lineto +395 414 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 365 422 moveto -363 412 lineto -359 422 lineto +newpath 400 419 moveto +405 410 lineto +395 414 lineto closepath stroke end grestore % tactics gsave 10 dict begin -164 662 45 25 ellipse_path +144 662 45 25 ellipse_path stroke gsave 10 dict begin -133 654 moveto +113 654 moveto (tactics) [6.72 10.56 10.56 6.72 6.72 10.56 9.36] xshow @@ -551,53 +518,53 @@ end grestore end grestore % tactics -> cic_unification -newpath 196 643 moveto -216 632 244 615 266 602 curveto +newpath 178 645 moveto +202 632 236 615 264 601 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 268 605 moveto -275 597 lineto -265 599 lineto +newpath 266 604 moveto +273 596 lineto +263 598 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 268 605 moveto -275 597 lineto -265 599 lineto +newpath 266 604 moveto +273 596 lineto +263 598 lineto closepath stroke end grestore % tactics -> whelp -newpath 164 636 moveto -164 628 164 619 164 610 curveto +newpath 150 637 moveto +152 628 154 618 156 609 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 168 610 moveto -164 600 lineto -161 610 lineto +newpath 159 609 moveto +158 599 lineto +153 608 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 168 610 moveto -164 600 lineto -161 610 lineto +newpath 159 609 moveto +158 599 lineto +153 608 lineto closepath stroke end grestore % paramodulation gsave 10 dict begin -191 750 90 25 ellipse_path +151 750 90 25 ellipse_path stroke gsave 10 dict begin -115 742 moveto +75 742 moveto (paramodulation) [12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12] xshow @@ -605,32 +572,32 @@ end grestore end grestore % paramodulation -> tactics -newpath 183 725 moveto -180 716 177 706 175 697 curveto +newpath 149 724 moveto +148 716 148 707 147 698 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 178 696 moveto -172 687 lineto -172 698 lineto +newpath 150 698 moveto +146 688 lineto +144 698 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 178 696 moveto -172 687 lineto -172 698 lineto +newpath 150 698 moveto +146 688 lineto +144 698 lineto closepath stroke end grestore % cic gsave 10 dict begin -359 298 28 25 ellipse_path +412 298 28 25 ellipse_path stroke gsave 10 dict begin -345 290 moveto +398 290 moveto (cic) [10.56 6.72 10.56] xshow @@ -639,10 +606,10 @@ end grestore % urimanager gsave 10 dict begin -353 210 70 25 ellipse_path +332 210 70 25 ellipse_path stroke gsave 10 dict begin -297 202 moveto +276 202 moveto (urimanager) [12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92] xshow @@ -650,32 +617,32 @@ end grestore end grestore % cic -> urimanager -newpath 357 272 moveto -356 264 356 255 355 246 curveto +newpath 394 278 moveto +384 267 372 254 361 241 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 359 246 moveto -355 236 lineto -352 246 lineto +newpath 364 239 moveto +354 234 lineto +359 244 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 359 246 moveto -355 236 lineto -352 246 lineto +newpath 364 239 moveto +354 234 lineto +359 244 lineto closepath stroke end grestore % xml gsave 10 dict begin -209 122 33 25 ellipse_path +431 122 33 25 ellipse_path stroke gsave 10 dict begin -190 114 moveto +412 114 moveto (xml) [12 18.72 6.72] xshow @@ -683,55 +650,53 @@ end grestore end grestore % cic -> xml -newpath 384 285 moveto -401 274 422 257 433 236 curveto -442 215 446 202 433 184 curveto -410 155 311 136 253 127 curveto +newpath 415 272 moveto +418 242 424 192 427 158 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 253 124 moveto -243 126 lineto -253 130 lineto +newpath 430 158 moveto +428 148 lineto +424 158 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 253 124 moveto -243 126 lineto -253 130 lineto +newpath 430 158 moveto +428 148 lineto +424 158 lineto closepath stroke end grestore % cic_proof_checking -> cic -newpath 363 360 moveto -362 352 362 343 361 334 curveto +newpath 433 361 moveto +430 352 427 342 423 333 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 365 334 moveto -361 324 lineto -358 334 lineto +newpath 426 332 moveto +420 323 lineto +420 334 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 365 334 moveto -361 324 lineto -358 334 lineto +newpath 426 332 moveto +420 323 lineto +420 334 lineto closepath stroke end grestore % getter gsave 10 dict begin -198 298 42 25 ellipse_path +274 298 42 25 ellipse_path stroke gsave 10 dict begin -170 290 moveto +246 290 moveto (getter) [12 10.56 6.72 6.72 10.56 7.92] xshow @@ -739,53 +704,53 @@ end grestore end grestore % cic_proof_checking -> getter -newpath 320 362 moveto -295 349 264 332 239 320 curveto +newpath 396 362 moveto +371 349 340 332 315 320 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 240 317 moveto -230 315 lineto -237 323 lineto +newpath 316 317 moveto +306 315 lineto +313 323 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 240 317 moveto -230 315 lineto -237 323 lineto +newpath 316 317 moveto +306 315 lineto +313 323 lineto closepath stroke end grestore % getter -> urimanager -newpath 229 280 moveto -251 268 281 250 306 237 curveto +newpath 290 274 moveto +296 265 304 254 310 244 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 308 240 moveto -315 232 lineto -305 234 lineto +newpath 313 245 moveto +316 235 lineto +308 241 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 308 240 moveto -315 232 lineto -305 234 lineto +newpath 313 245 moveto +316 235 lineto +308 241 lineto closepath stroke end grestore % registry gsave 10 dict begin -83 210 52 25 ellipse_path +190 210 52 25 ellipse_path stroke gsave 10 dict begin -45 202 moveto +152 202 moveto (registry) [7.92 10.56 12 6.72 9.36 6.72 7.92 12] xshow @@ -793,32 +758,32 @@ end grestore end grestore % getter -> registry -newpath 172 278 moveto -157 266 137 251 119 238 curveto +newpath 253 276 moveto +243 265 230 252 219 240 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 121 235 moveto -111 232 lineto -117 241 lineto +newpath 222 238 moveto +212 233 lineto +217 243 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 121 235 moveto -111 232 lineto -117 241 lineto +newpath 222 238 moveto +212 233 lineto +217 243 lineto closepath stroke end grestore % metadata gsave 10 dict begin -83 386 58 25 ellipse_path +159 386 58 25 ellipse_path stroke gsave 10 dict begin -39 378 moveto +115 378 moveto (metadata) [18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] xshow @@ -826,54 +791,54 @@ end grestore end grestore % metadata -> cic -newpath 127 369 moveto -135 366 143 363 151 360 curveto -210 340 279 319 321 308 curveto +newpath 203 369 moveto +211 366 219 363 227 360 curveto +277 342 337 322 374 310 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 322 311 moveto -331 305 lineto -320 305 lineto +newpath 375 313 moveto +384 307 lineto +373 307 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 322 311 moveto -331 305 lineto -320 305 lineto +newpath 375 313 moveto +384 307 lineto +373 307 lineto closepath stroke end grestore % metadata -> getter -newpath 112 364 moveto -127 352 147 337 164 324 curveto +newpath 188 364 moveto +203 352 223 337 240 324 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 166 327 moveto -172 318 lineto -162 321 lineto +newpath 242 327 moveto +248 318 lineto +238 321 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 166 327 moveto -172 318 lineto -162 321 lineto +newpath 242 327 moveto +248 318 lineto +238 321 lineto closepath stroke end grestore % hmysql gsave 10 dict begin -83 298 50 25 ellipse_path +161 298 50 25 ellipse_path stroke gsave 10 dict begin -47 290 moveto +125 290 moveto (hmysql) [12 18.72 12 9.36 12 6.72] xshow @@ -881,54 +846,53 @@ end grestore end grestore % metadata -> hmysql -newpath 83 360 moveto -83 352 83 343 83 334 curveto +newpath 160 360 moveto +160 352 160 343 160 334 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 87 334 moveto -83 324 lineto -80 334 lineto +newpath 164 334 moveto +160 324 lineto +157 334 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 87 334 moveto -83 324 lineto -80 334 lineto +newpath 164 334 moveto +160 324 lineto +157 334 lineto closepath stroke end grestore % whelp -> metadata -newpath 165 548 moveto -164 522 161 480 145 448 curveto -139 436 129 425 119 415 curveto +newpath 163 548 moveto +162 515 161 459 160 422 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 122 413 moveto -112 408 lineto -117 418 lineto +newpath 164 422 moveto +160 412 lineto +157 422 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 122 413 moveto -112 408 lineto -117 418 lineto +newpath 164 422 moveto +160 412 lineto +157 422 lineto closepath stroke end grestore % extlib gsave 10 dict begin -209 34 42 25 ellipse_path +431 34 42 25 ellipse_path stroke gsave 10 dict begin -181 26 moveto +403 26 moveto (extlib) [10.56 12 6.72 6.72 6.72 12] xshow @@ -937,10 +901,10 @@ end grestore % hgdome gsave 10 dict begin -209 210 54 25 ellipse_path +571 210 54 25 ellipse_path stroke gsave 10 dict begin -169 202 moveto +531 202 moveto (hgdome) [12 12 12 12 18.72 10.56] xshow @@ -948,85 +912,86 @@ end grestore end grestore % hgdome -> xml -newpath 209 184 moveto -209 176 209 167 209 158 curveto +newpath 538 189 moveto +517 176 488 158 466 144 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 213 158 moveto -209 148 lineto -206 158 lineto +newpath 468 141 moveto +458 139 lineto +465 147 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 213 158 moveto -209 148 lineto -206 158 lineto +newpath 468 141 moveto +458 139 lineto +465 147 lineto closepath stroke end grestore % hmysql -> registry -newpath 83 272 moveto -83 264 83 255 83 246 curveto +newpath 169 273 moveto +172 264 175 254 179 245 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 87 246 moveto -83 236 lineto -80 246 lineto +newpath 182 246 moveto +182 235 lineto +176 244 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 87 246 moveto -83 236 lineto -80 246 lineto +newpath 182 246 moveto +182 235 lineto +176 244 lineto closepath stroke end grestore % registry -> xml -newpath 113 189 moveto -132 176 157 159 176 145 curveto +newpath 229 193 moveto +237 190 245 187 252 184 curveto +299 166 354 147 390 135 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 178 148 moveto -184 139 lineto -174 142 lineto +newpath 391 138 moveto +400 132 lineto +389 132 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 178 148 moveto -184 139 lineto -174 142 lineto +newpath 391 138 moveto +400 132 lineto +389 132 lineto closepath stroke end grestore % xml -> extlib -newpath 209 96 moveto -209 88 209 79 209 70 curveto +newpath 431 96 moveto +431 88 431 79 431 70 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 213 70 moveto -209 60 lineto -206 70 lineto +newpath 435 70 moveto +431 60 lineto +428 70 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 213 70 moveto -209 60 lineto -206 70 lineto +newpath 435 70 moveto +431 60 lineto +428 70 lineto closepath stroke end grestore @@ -1063,22 +1028,22 @@ end grestore end grestore % DependencyAnalyzer -> metadata -newpath 73 448 moveto -74 439 76 430 77 422 curveto +newpath 99 448 moveto +109 438 119 427 129 417 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 80 422 moveto -79 412 lineto -74 421 lineto +newpath 131 420 moveto +136 410 lineto +126 415 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 80 422 moveto -79 412 lineto -74 421 lineto +newpath 131 420 moveto +136 410 lineto +126 415 lineto closepath stroke end grestore @@ -1088,22 +1053,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 236 404 moveto -160 404 lineto -160 368 lineto +newpath 312 404 moveto +236 404 lineto 236 368 lineto +312 368 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 236 404 moveto -160 404 lineto -160 368 lineto +newpath 312 404 moveto +236 404 lineto 236 368 lineto +312 368 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -168 378 moveto +244 378 moveto (Getter) [17.28 10.56 6.72 6.72 10.56 7.92] xshow @@ -1111,22 +1076,22 @@ end grestore end grestore % Getter -> getter -newpath 198 368 moveto -198 358 198 346 198 334 curveto +newpath 274 368 moveto +274 358 274 346 274 334 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 202 334 moveto -198 324 lineto -195 334 lineto +newpath 278 334 moveto +274 324 lineto +271 334 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 202 334 moveto -198 324 lineto -195 334 lineto +newpath 278 334 moveto +274 324 lineto +271 334 lineto closepath stroke end grestore @@ -1136,22 +1101,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 363 848 moveto -285 848 lineto -285 812 lineto -363 812 lineto +newpath 454 848 moveto +376 848 lineto +376 812 lineto +454 812 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 363 848 moveto -285 848 lineto -285 812 lineto -363 812 lineto +newpath 454 848 moveto +376 848 lineto +376 812 lineto +454 812 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -292 822 moveto +383 822 moveto (Matita) [21.36 10.56 6.72 6.72 6.72 10.56] xshow @@ -1159,65 +1124,89 @@ end grestore end grestore % Matita -> cic_disambiguation -newpath 326 812 moveto -328 785 332 733 335 698 curveto +newpath 376 815 moveto +343 801 300 783 296 776 curveto +281 752 289 721 299 696 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 338 698 moveto -336 688 lineto -332 698 lineto +newpath 302 698 moveto +303 687 lineto +296 695 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 338 698 moveto -336 688 lineto -332 698 lineto +newpath 302 698 moveto +303 687 lineto +296 695 lineto closepath stroke end grestore % Matita -> grafite -newpath 363 823 moveto -408 814 483 797 545 776 curveto -549 774 553 773 556 771 curveto +newpath 447 812 moveto +466 801 491 786 512 774 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 558 774 moveto -566 767 lineto -555 767 lineto +newpath 514 777 moveto +521 769 lineto +511 771 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 558 774 moveto -566 767 lineto -555 767 lineto +newpath 514 777 moveto +521 769 lineto +511 771 lineto closepath stroke end grestore % Matita -> paramodulation -newpath 294 812 moveto -278 802 257 789 239 778 curveto +newpath 376 818 moveto +336 806 272 787 223 772 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 224 769 moveto +213 769 lineto +222 775 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 224 769 moveto +213 769 lineto +222 775 lineto +closepath +stroke +end grestore + +% Matita -> hgdome +newpath 454 827 moveto +524 814 562 831 610 776 curveto +643 737 629 713 629 662 curveto +629 662 629 662 629 386 curveto +629 334 606 278 590 244 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 240 775 moveto -230 773 lineto -237 781 lineto +newpath 593 242 moveto +585 235 lineto +587 245 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 240 775 moveto -230 773 lineto -237 781 lineto +newpath 593 242 moveto +585 235 lineto +587 245 lineto closepath stroke end grestore @@ -1227,26 +1216,26 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 337 512 moveto -241 512 lineto -241 448 lineto -337 448 lineto +newpath 601 512 moveto +505 512 lineto +505 448 lineto +601 448 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 337 512 moveto -241 512 lineto -241 448 lineto -337 448 lineto +newpath 601 512 moveto +505 512 lineto +505 448 lineto +601 448 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -262 486 moveto +526 486 moveto (Proof) [13.44 7.92 12 12 7.92] xshow -249 458 moveto +513 458 moveto (Checker) [16.08 12 10.56 10.56 12 10.56 7.92] xshow @@ -1254,22 +1243,22 @@ end grestore end grestore % ProofChecker -> cic_proof_checking -newpath 315 448 moveto -323 439 331 429 339 419 curveto +newpath 515 448 moveto +503 438 490 427 478 417 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 342 421 moveto -345 411 lineto -336 417 lineto +newpath 480 414 moveto +470 411 lineto +476 420 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 342 421 moveto -345 411 lineto -336 417 lineto +newpath 480 414 moveto +470 411 lineto +476 420 lineto closepath stroke end grestore @@ -1279,22 +1268,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 536 768 moveto -450 768 lineto -450 732 lineto -536 732 lineto +newpath 489 768 moveto +403 768 lineto +403 732 lineto +489 732 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 536 768 moveto -450 768 lineto -450 732 lineto -536 732 lineto +newpath 489 768 moveto +403 768 lineto +403 732 lineto +489 732 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -457 742 moveto +410 742 moveto (Uwobo) [17.28 17.28 12 12 12] xshow @@ -1302,22 +1291,22 @@ end grestore end grestore % Uwobo -> content_pres -newpath 503 732 moveto -509 722 517 708 524 696 curveto +newpath 462 732 moveto +472 721 484 707 495 695 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 527 697 moveto -529 687 lineto -521 694 lineto +newpath 498 697 moveto +502 687 lineto +493 692 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 527 697 moveto -529 687 lineto -521 694 lineto +newpath 498 697 moveto +502 687 lineto +493 692 lineto closepath stroke end grestore @@ -1327,22 +1316,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 432 768 moveto -352 768 lineto -352 732 lineto -432 732 lineto +newpath 385 768 moveto +305 768 lineto +305 732 lineto +385 732 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 432 768 moveto -352 768 lineto -352 732 lineto -432 732 lineto +newpath 385 768 moveto +305 768 lineto +305 732 lineto +385 732 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -359 742 moveto +312 742 moveto (Whelp) [22.56 12 10.56 6.72 12] xshow @@ -1350,43 +1339,44 @@ end grestore end grestore % Whelp -> cic_disambiguation -newpath 381 732 moveto -375 722 366 708 359 696 curveto +newpath 339 732 moveto +336 722 332 709 329 698 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 362 694 moveto -354 687 lineto -356 697 lineto +newpath 332 697 moveto +326 688 lineto +326 699 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 362 694 moveto -354 687 lineto -356 697 lineto +newpath 332 697 moveto +326 688 lineto +326 699 lineto closepath stroke end grestore % Whelp -> content_pres -newpath 423 732 moveto -444 720 472 703 496 689 curveto +newpath 378 732 moveto +383 729 389 726 394 724 curveto +418 712 446 699 469 687 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 498 692 moveto -505 684 lineto -495 686 lineto +newpath 470 690 moveto +478 683 lineto +467 684 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 498 692 moveto -505 684 lineto -495 686 lineto +newpath 470 690 moveto +478 683 lineto +467 684 lineto closepath stroke end grestore diff --git a/helm/papers/matita/librariesCluster.ps b/helm/papers/matita/librariesCluster.ps index eb52d37d1..2fd94573d 100644 --- a/helm/papers/matita/librariesCluster.ps +++ b/helm/papers/matita/librariesCluster.ps @@ -3,7 +3,7 @@ %%For: (zacchiro) Stefano Zacchiroli,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 1114 979 +%%BoundingBox: 35 35 1258 979 %%EndComments save %%BeginProlog @@ -230,10 +230,10 @@ def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 1114 979 +%%PageBoundingBox: 36 36 1258 979 %%PageOrientation: Portrait gsave -35 35 1079 944 boxprim clip newpath +35 35 1223 944 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0 0 translate 0 rotate @@ -244,22 +244,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 640 488 moveto -1069 488 lineto -1069 862 lineto -640 862 lineto +newpath 764 488 moveto +1193 488 lineto +1193 862 lineto +764 862 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 640 488 moveto -1069 488 lineto -1069 862 lineto -640 862 lineto +newpath 764 488 moveto +1193 488 lineto +1193 862 lineto +764 862 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -648 498 moveto +772 498 moveto (Terms at the content and presentation level) [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] xshow @@ -270,22 +270,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 152 618 moveto -402 618 lineto -402 898 lineto -152 898 lineto +newpath 314 618 moveto +564 618 lineto +564 898 lineto +314 898 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 152 618 moveto -402 618 lineto -402 898 lineto -152 898 lineto +newpath 314 618 moveto +564 618 lineto +564 898 lineto +314 898 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -160 872 moveto +322 872 moveto (Partially specified terms) [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] xshow @@ -296,22 +296,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 258 208 moveto -632 208 lineto -632 592 lineto -258 592 lineto +newpath 86 208 moveto +460 208 lineto +460 592 lineto +86 592 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 258 208 moveto -632 208 lineto -632 592 lineto -258 592 lineto +newpath 86 208 moveto +460 208 lineto +460 592 lineto +86 592 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -265 218 moveto +93 218 moveto (Fully specified terms) [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] xshow @@ -322,22 +322,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 640 16 moveto -928 16 lineto -928 400 lineto -640 400 lineto +newpath 468 16 moveto +718 16 lineto +718 400 lineto +468 400 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 640 16 moveto -928 16 lineto -928 400 lineto -640 400 lineto +newpath 468 16 moveto +718 16 lineto +718 400 lineto +468 400 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -842 26 moveto +632 26 moveto (Utilities) [17.28 6.72 6.72 6.72 6.72 6.72 6.72 10.56 9.36] xshow @@ -346,10 +346,10 @@ end grestore % acic_content gsave 10 dict begin -758 652 75 25 ellipse_path +849 652 75 25 ellipse_path stroke gsave 10 dict begin -697 644 moveto +788 644 moveto (acic_content) [10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72] xshow @@ -358,10 +358,10 @@ end grestore % cic_acic gsave 10 dict begin -731 558 54 25 ellipse_path +839 558 54 25 ellipse_path stroke gsave 10 dict begin -691 550 moveto +799 550 moveto (cic_acic) [10.56 6.72 10.56 12 10.56 10.56 6.72 10.56] xshow @@ -369,32 +369,32 @@ end grestore end grestore % acic_content -> cic_acic -newpath 751 626 moveto -748 616 744 604 741 593 curveto +newpath 846 626 moveto +845 616 844 605 843 594 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 744 592 moveto -739 583 lineto -738 593 lineto +newpath 846 594 moveto +842 584 lineto +840 594 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 744 592 moveto -739 583 lineto -738 593 lineto +newpath 846 594 moveto +842 584 lineto +840 594 lineto closepath stroke end grestore % cic_proof_checking gsave 10 dict begin -513 454 110 25 ellipse_path +341 454 110 25 ellipse_path stroke gsave 10 dict begin -417 446 moveto +245 446 moveto (cic_proof_checking) [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] xshow @@ -402,33 +402,33 @@ end grestore end grestore % cic_acic -> cic_proof_checking -newpath 706 535 moveto -688 520 662 500 636 488 curveto -626 483 615 479 604 475 curveto +newpath 820 534 moveto +806 518 784 497 760 488 curveto +741 480 423 491 361 482 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 605 472 moveto -594 472 lineto -603 478 lineto +newpath 361 479 moveto +351 480 lineto +360 485 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 605 472 moveto -594 472 lineto -603 478 lineto +newpath 361 479 moveto +351 480 lineto +360 485 lineto closepath stroke end grestore % cic_disambiguation gsave 10 dict begin -758 740 109 25 ellipse_path +1054 740 109 25 ellipse_path stroke gsave 10 dict begin -663 732 moveto +959 732 moveto (cic_disambiguation) [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] xshow @@ -436,32 +436,32 @@ end grestore end grestore % cic_disambiguation -> acic_content -newpath 758 714 moveto -758 706 758 697 758 688 curveto +newpath 975 722 moveto +935 712 890 698 867 684 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 762 688 moveto -758 678 lineto -755 688 lineto +newpath 869 681 moveto +859 678 lineto +865 687 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 762 688 moveto -758 678 lineto -755 688 lineto +newpath 869 681 moveto +859 678 lineto +865 687 lineto closepath stroke end grestore % cic_unification gsave 10 dict begin -307 652 86 25 ellipse_path +469 652 86 25 ellipse_path stroke gsave 10 dict begin -235 644 moveto +397 644 moveto (cic_unification) [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] xshow @@ -469,32 +469,34 @@ end grestore end grestore % cic_disambiguation -> cic_unification -newpath 674 724 moveto -592 708 471 684 390 668 curveto +newpath 976 722 moveto +963 719 948 716 935 714 curveto +810 692 777 695 650 678 curveto +619 674 586 669 557 665 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 390 665 moveto -380 666 lineto -389 671 lineto +newpath 557 662 moveto +547 663 lineto +556 668 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 390 665 moveto -380 666 lineto -389 671 lineto +newpath 557 662 moveto +547 663 lineto +556 668 lineto closepath stroke end grestore % whelp gsave 10 dict begin -325 558 44 25 ellipse_path +354 558 44 25 ellipse_path stroke gsave 10 dict begin -295 550 moveto +324 550 moveto (whelp) [17.28 12 10.56 6.72 12] xshow @@ -502,32 +504,38 @@ end grestore end grestore % cic_disambiguation -> whelp -newpath 704 718 moveto -618 681 451 611 370 577 curveto +newpath 968 724 moveto +968 723 967 723 967 723 curveto +965 721 964 721 961 720 curveto +932 706 922 708 890 702 curveto +835 690 820 691 764 678 curveto +676 656 658 637 568 618 curveto +524 608 402 620 366 592 curveto +366 592 366 592 365 592 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 372 574 moveto -361 573 lineto -369 580 lineto +newpath 368 590 moveto +360 583 lineto +362 593 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 372 574 moveto -361 573 lineto -369 580 lineto +newpath 368 590 moveto +360 583 lineto +362 593 lineto closepath stroke end grestore % content_pres gsave 10 dict begin -963 740 76 25 ellipse_path +849 740 76 25 ellipse_path stroke gsave 10 dict begin -901 732 moveto +787 732 moveto (content_pres) [10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] xshow @@ -535,65 +543,32 @@ end grestore end grestore % content_pres -> acic_content -newpath 916 720 moveto -885 707 846 690 814 676 curveto +newpath 849 714 moveto +849 706 849 697 849 688 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 816 673 moveto -805 672 lineto -813 679 lineto +newpath 853 688 moveto +849 678 lineto +846 688 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 816 673 moveto -805 672 lineto -813 679 lineto -closepath -stroke -end grestore - -% utf8_macros -gsave 10 dict begin -844 366 75 25 ellipse_path -stroke -gsave 10 dict begin -783 358 moveto -(utf8_macros) -[12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36] -xshow -end grestore -end grestore - -% content_pres -> utf8_macros -newpath 955 715 moveto -934 649 879 476 855 401 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 858 400 moveto -852 391 lineto -852 402 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 858 400 moveto -852 391 lineto -852 402 lineto +newpath 853 688 moveto +849 678 lineto +846 688 lineto closepath stroke end grestore % grafite gsave 10 dict begin -830 828 46 25 ellipse_path +881 828 46 25 ellipse_path stroke gsave 10 dict begin -798 820 moveto +849 820 moveto (grafite) [12 7.92 10.56 7.92 6.72 6.72 10.56] xshow @@ -601,54 +576,58 @@ end grestore end grestore % grafite -> content_pres -newpath 860 808 moveto -877 797 900 782 920 769 curveto +newpath 872 803 moveto +868 794 865 784 861 775 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 922 772 moveto -928 763 lineto -918 766 lineto +newpath 864 774 moveto +858 765 lineto +858 776 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 922 772 moveto -928 763 lineto -918 766 lineto +newpath 864 774 moveto +858 765 lineto +858 776 lineto closepath stroke end grestore % cic_unification -> cic_proof_checking -newpath 337 628 moveto -350 617 366 604 379 592 curveto -416 557 456 515 483 487 curveto +newpath 552 644 moveto +622 636 714 620 736 592 curveto +765 555 769 521 736 488 curveto +731 482 606 483 598 483 curveto +563 482 555 482 519 482 curveto +503 481 389 482 372 481 curveto +372 481 372 481 372 481 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 486 489 moveto -490 479 lineto -481 484 lineto +newpath 376 478 moveto +365 479 lineto +374 485 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 486 489 moveto -490 479 lineto -481 484 lineto +newpath 376 478 moveto +365 479 lineto +374 485 lineto closepath stroke end grestore % tactics gsave 10 dict begin -301 740 45 25 ellipse_path +463 740 45 25 ellipse_path stroke gsave 10 dict begin -270 732 moveto +432 732 moveto (tactics) [6.72 10.56 10.56 6.72 6.72 10.56 9.36] xshow @@ -656,56 +635,54 @@ end grestore end grestore % tactics -> cic_unification -newpath 303 714 moveto -304 706 304 697 305 688 curveto +newpath 465 714 moveto +466 706 466 697 467 688 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 309 688 moveto -305 678 lineto -302 688 lineto +newpath 471 688 moveto +467 678 lineto +464 688 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 309 688 moveto -305 678 lineto -302 688 lineto +newpath 471 688 moveto +467 678 lineto +464 688 lineto closepath stroke end grestore % tactics -> whelp -newpath 264 725 moveto -245 714 222 699 211 678 curveto -199 654 196 639 211 618 curveto -230 591 252 607 280 592 curveto -284 590 288 588 291 585 curveto +newpath 427 724 moveto +408 714 386 698 373 678 curveto +357 653 353 620 353 594 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 293 588 moveto -299 579 lineto -289 582 lineto +newpath 357 594 moveto +353 584 lineto +350 594 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 293 588 moveto -299 579 lineto -289 582 lineto +newpath 357 594 moveto +353 584 lineto +350 594 lineto closepath stroke end grestore % paramodulation gsave 10 dict begin -301 828 90 25 ellipse_path +463 828 90 25 ellipse_path stroke gsave 10 dict begin -225 820 moveto +387 820 moveto (paramodulation) [12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12] xshow @@ -713,32 +690,32 @@ end grestore end grestore % paramodulation -> tactics -newpath 301 802 moveto -301 794 301 785 301 776 curveto +newpath 463 802 moveto +463 794 463 785 463 776 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 305 776 moveto -301 766 lineto -298 776 lineto +newpath 467 776 moveto +463 766 lineto +460 776 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 305 776 moveto -301 766 lineto -298 776 lineto +newpath 467 776 moveto +463 766 lineto +460 776 lineto closepath stroke end grestore % cic gsave 10 dict begin -420 366 28 25 ellipse_path +248 366 28 25 ellipse_path stroke gsave 10 dict begin -406 358 moveto +234 358 moveto (cic) [10.56 6.72 10.56] xshow @@ -747,10 +724,10 @@ end grestore % urimanager gsave 10 dict begin -515 278 70 25 ellipse_path +343 278 70 25 ellipse_path stroke gsave 10 dict begin -459 270 moveto +287 270 moveto (urimanager) [12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92] xshow @@ -758,32 +735,32 @@ end grestore end grestore % cic -> urimanager -newpath 440 347 moveto -452 336 468 322 482 309 curveto +newpath 268 347 moveto +280 336 296 322 310 309 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 484 312 moveto -489 302 lineto -479 307 lineto +newpath 312 312 moveto +317 302 lineto +307 307 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 484 312 moveto -489 302 lineto -479 307 lineto +newpath 312 312 moveto +317 302 lineto +307 307 lineto closepath stroke end grestore % xml gsave 10 dict begin -701 174 33 25 ellipse_path +529 174 33 25 ellipse_path stroke gsave 10 dict begin -682 166 moveto +510 166 moveto (xml) [12 18.72 6.72] xshow @@ -791,54 +768,54 @@ end grestore end grestore % cic -> xml -newpath 414 341 moveto -407 306 401 243 435 208 curveto -450 192 585 181 657 177 curveto +newpath 242 341 moveto +235 306 229 243 263 208 curveto +278 192 413 181 485 177 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 657 180 moveto -667 176 lineto -657 174 lineto +newpath 485 180 moveto +495 176 lineto +485 174 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 657 180 moveto -667 176 lineto -657 174 lineto +newpath 485 180 moveto +495 176 lineto +485 174 lineto closepath stroke end grestore % cic_proof_checking -> cic -newpath 487 429 moveto -475 417 460 404 448 392 curveto +newpath 315 429 moveto +303 417 288 404 276 392 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 450 389 moveto -440 385 lineto -445 394 lineto +newpath 278 389 moveto +268 385 lineto +273 394 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 450 389 moveto -440 385 lineto -445 394 lineto +newpath 278 389 moveto +268 385 lineto +273 394 lineto closepath stroke end grestore % getter gsave 10 dict begin -513 366 42 25 ellipse_path +341 366 42 25 ellipse_path stroke gsave 10 dict begin -485 358 moveto +313 358 moveto (getter) [12 10.56 6.72 6.72 10.56 7.92] xshow @@ -846,53 +823,53 @@ end grestore end grestore % cic_proof_checking -> getter -newpath 513 428 moveto -513 420 513 411 513 402 curveto +newpath 341 428 moveto +341 420 341 411 341 402 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 517 402 moveto -513 392 lineto -510 402 lineto +newpath 345 402 moveto +341 392 lineto +338 402 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 517 402 moveto -513 392 lineto -510 402 lineto +newpath 345 402 moveto +341 392 lineto +338 402 lineto closepath stroke end grestore % getter -> urimanager -newpath 514 340 moveto -514 332 514 323 514 314 curveto +newpath 342 340 moveto +342 332 342 323 342 314 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 518 314 moveto -514 304 lineto -511 314 lineto +newpath 346 314 moveto +342 304 lineto +339 314 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 518 314 moveto -514 304 lineto -511 314 lineto +newpath 346 314 moveto +342 304 lineto +339 314 lineto closepath stroke end grestore % registry gsave 10 dict begin -701 278 52 25 ellipse_path +529 278 52 25 ellipse_path stroke gsave 10 dict begin -663 270 moveto +491 270 moveto (registry) [7.92 10.56 12 6.72 9.36 6.72 7.92 12] xshow @@ -900,32 +877,32 @@ end grestore end grestore % getter -> registry -newpath 547 350 moveto -577 336 621 316 654 300 curveto +newpath 375 350 moveto +405 336 449 316 482 300 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 655 303 moveto -663 296 lineto -652 297 lineto +newpath 483 303 moveto +491 296 lineto +480 297 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 655 303 moveto -663 296 lineto -652 297 lineto +newpath 483 303 moveto +491 296 lineto +480 297 lineto closepath stroke end grestore % metadata gsave 10 dict begin -325 454 58 25 ellipse_path +153 454 58 25 ellipse_path stroke gsave 10 dict begin -281 446 moveto +109 446 moveto (metadata) [18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] xshow @@ -933,54 +910,54 @@ end grestore end grestore % metadata -> cic -newpath 350 431 moveto -363 419 379 404 392 392 curveto +newpath 178 431 moveto +191 419 207 404 220 392 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 395 394 moveto -400 385 lineto -390 389 lineto +newpath 223 394 moveto +228 385 lineto +218 389 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 395 394 moveto -400 385 lineto -390 389 lineto +newpath 223 394 moveto +228 385 lineto +218 389 lineto closepath stroke end grestore % metadata -> getter -newpath 369 437 moveto -401 424 442 408 458 400 curveto -464 397 470 394 475 390 curveto +newpath 197 437 moveto +229 424 270 408 286 400 curveto +292 397 298 394 303 390 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 477 393 moveto -484 385 lineto -474 387 lineto +newpath 305 393 moveto +312 385 lineto +302 387 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 477 393 moveto -484 385 lineto -474 387 lineto +newpath 305 393 moveto +312 385 lineto +302 387 lineto closepath stroke end grestore % hmysql gsave 10 dict begin -699 366 50 25 ellipse_path +528 366 50 25 ellipse_path stroke gsave 10 dict begin -663 358 moveto +492 358 moveto (hmysql) [12 18.72 12 9.36 12 6.72] xshow @@ -988,55 +965,55 @@ end grestore end grestore % metadata -> hmysql -newpath 367 436 moveto -375 433 384 430 393 428 curveto -499 402 533 432 636 400 curveto -644 398 651 394 658 391 curveto +newpath 195 436 moveto +203 433 212 430 221 428 curveto +327 402 361 432 464 400 curveto +472 397 479 394 487 390 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 660 394 moveto -667 386 lineto -657 388 lineto +newpath 488 393 moveto +496 386 lineto +485 387 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 660 394 moveto -667 386 lineto -657 388 lineto +newpath 488 393 moveto +496 386 lineto +485 387 lineto closepath stroke end grestore % whelp -> metadata -newpath 325 532 moveto -325 519 325 504 325 490 curveto +newpath 320 541 moveto +287 523 237 497 200 479 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 329 490 moveto -325 480 lineto -322 490 lineto +newpath 201 476 moveto +191 474 lineto +198 482 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 329 490 moveto -325 480 lineto -322 490 lineto +newpath 201 476 moveto +191 474 lineto +198 482 lineto closepath stroke end grestore % extlib gsave 10 dict begin -701 86 42 25 ellipse_path +529 86 42 25 ellipse_path stroke gsave 10 dict begin -673 78 moveto +501 78 moveto (extlib) [10.56 12 6.72 6.72 6.72 12] xshow @@ -1045,10 +1022,10 @@ end grestore % hgdome gsave 10 dict begin -827 278 54 25 ellipse_path +655 278 54 25 ellipse_path stroke gsave 10 dict begin -787 270 moveto +615 270 moveto (hgdome) [12 12 12 12 18.72 10.56] xshow @@ -1056,86 +1033,86 @@ end grestore end grestore % hgdome -> xml -newpath 809 254 moveto -797 239 780 221 763 208 curveto -756 202 747 197 739 192 curveto +newpath 637 254 moveto +625 239 608 221 591 208 curveto +584 202 575 197 567 192 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 740 189 moveto -730 187 lineto -737 195 lineto +newpath 568 189 moveto +558 187 lineto +565 195 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 740 189 moveto -730 187 lineto -737 195 lineto +newpath 568 189 moveto +558 187 lineto +565 195 lineto closepath stroke end grestore % hmysql -> registry -newpath 700 340 moveto -700 332 700 323 700 314 curveto +newpath 528 340 moveto +528 332 529 323 529 314 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 704 314 moveto -700 304 lineto -697 314 lineto +newpath 533 314 moveto +529 304 lineto +526 314 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 704 314 moveto -700 304 lineto -697 314 lineto +newpath 533 314 moveto +529 304 lineto +526 314 lineto closepath stroke end grestore % registry -> xml -newpath 701 252 moveto -701 239 701 224 701 210 curveto +newpath 529 252 moveto +529 239 529 224 529 210 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 705 210 moveto -701 200 lineto -698 210 lineto +newpath 533 210 moveto +529 200 lineto +526 210 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 705 210 moveto -701 200 lineto -698 210 lineto +newpath 533 210 moveto +529 200 lineto +526 210 lineto closepath stroke end grestore % xml -> extlib -newpath 701 148 moveto -701 140 701 131 701 122 curveto +newpath 529 148 moveto +529 140 529 131 529 122 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 705 122 moveto -701 112 lineto -698 122 lineto +newpath 533 122 moveto +529 112 lineto +526 122 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 705 122 moveto -701 112 lineto -698 122 lineto +newpath 533 122 moveto +529 112 lineto +526 122 lineto closepath stroke end grestore @@ -1145,26 +1122,26 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 136 590 moveto -0 590 lineto -0 526 lineto -136 526 lineto +newpath 604 590 moveto +468 590 lineto +468 526 lineto +604 526 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 136 590 moveto -0 590 lineto -0 526 lineto -136 526 lineto +newpath 604 590 moveto +468 590 lineto +468 526 lineto +604 526 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -8 564 moveto +476 564 moveto (Dependency) [17.28 10.56 12 10.56 12 12 10.56 12 10.56 12] xshow -24 536 moveto +492 536 moveto (Analyzer) [17.28 12 10.56 6.72 12 10.56 10.56 7.92] xshow @@ -1172,24 +1149,24 @@ end grestore end grestore % DependencyAnalyzer -> metadata -newpath 94 526 moveto -108 512 126 496 145 488 curveto -170 477 240 486 266 480 curveto -270 479 273 478 277 477 curveto +newpath 513 526 moveto +500 511 483 496 464 488 curveto +440 477 248 485 221 480 curveto +216 479 210 477 205 475 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 278 480 moveto -286 473 lineto -275 474 lineto +newpath 206 472 moveto +195 472 lineto +204 478 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 278 480 moveto -286 473 lineto -275 474 lineto +newpath 206 472 moveto +195 472 lineto +204 478 lineto closepath stroke end grestore @@ -1199,22 +1176,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 248 472 moveto -172 472 lineto -172 436 lineto -248 436 lineto +newpath 76 472 moveto +0 472 lineto +0 436 lineto +76 436 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 248 472 moveto -172 472 lineto -172 436 lineto -248 436 lineto +newpath 76 472 moveto +0 472 lineto +0 436 lineto +76 436 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -180 446 moveto +8 446 moveto (Getter) [17.28 10.56 6.72 6.72 10.56 7.92] xshow @@ -1222,24 +1199,24 @@ end grestore end grestore % Getter -> getter -newpath 237 436 moveto -242 433 248 430 254 428 curveto -341 397 372 430 458 400 curveto -465 397 471 394 477 391 curveto +newpath 65 436 moveto +70 433 76 430 82 428 curveto +169 397 200 430 286 400 curveto +293 397 299 394 305 391 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 479 394 moveto -486 386 lineto -476 388 lineto +newpath 307 394 moveto +314 386 lineto +304 388 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 479 394 moveto -486 386 lineto -476 388 lineto +newpath 307 394 moveto +314 386 lineto +304 388 lineto closepath stroke end grestore @@ -1249,22 +1226,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 459 942 moveto -381 942 lineto -381 906 lineto -459 906 lineto +newpath 990 942 moveto +912 942 lineto +912 906 lineto +990 906 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 459 942 moveto -381 942 lineto -381 906 lineto -459 906 lineto +newpath 990 942 moveto +912 942 lineto +912 906 lineto +990 906 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -388 916 moveto +919 916 moveto (Matita) [21.36 10.56 6.72 6.72 6.72 10.56] xshow @@ -1272,67 +1249,90 @@ end grestore end grestore % Matita -> cic_disambiguation -newpath 417 906 moveto -415 879 414 830 439 802 curveto -504 731 554 751 640 746 curveto +newpath 961 906 moveto +978 875 1012 813 1035 775 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 640 749 moveto -650 745 lineto -640 743 lineto +newpath 1038 776 moveto +1040 766 lineto +1032 773 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 640 749 moveto -650 745 lineto -640 743 lineto +newpath 1038 776 moveto +1040 766 lineto +1032 773 lineto closepath stroke end grestore % Matita -> grafite -newpath 459 923 moveto -547 921 756 914 783 898 curveto -798 890 808 876 816 862 curveto +newpath 912 914 moveto +904 910 896 905 891 898 curveto +883 889 880 876 879 864 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 819 864 moveto -820 853 lineto -813 861 lineto +newpath 883 864 moveto +879 854 lineto +876 864 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 819 864 moveto -820 853 lineto -813 861 lineto +newpath 883 864 moveto +879 854 lineto +876 864 lineto closepath stroke end grestore % Matita -> paramodulation -newpath 381 919 moveto -354 915 321 908 311 898 curveto -302 889 299 876 298 864 curveto +newpath 912 923 moveto +801 921 489 912 473 898 curveto +464 889 460 877 459 864 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 463 864 moveto +459 854 lineto +456 864 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 463 864 moveto +459 854 lineto +456 864 lineto +closepath +stroke +end grestore + +% Matita -> hgdome +newpath 990 922 moveto +1056 919 1183 912 1197 898 curveto +1221 872 1211 775 1211 740 curveto +1211 740 1211 740 1211 454 curveto +1211 351 865 301 719 284 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 302 864 moveto -298 854 lineto -295 864 lineto +newpath 719 281 moveto +709 283 lineto +719 287 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 302 864 moveto -298 854 lineto -295 864 lineto +newpath 719 281 moveto +709 283 lineto +719 287 lineto closepath stroke end grestore @@ -1342,26 +1342,26 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 250 590 moveto -154 590 lineto -154 526 lineto -250 526 lineto +newpath 718 590 moveto +622 590 lineto +622 526 lineto +718 526 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 250 590 moveto -154 590 lineto -154 526 lineto -250 526 lineto +newpath 718 590 moveto +622 590 lineto +622 526 lineto +718 526 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -175 564 moveto +643 564 moveto (Proof) [13.44 7.92 12 12 7.92] xshow -162 536 moveto +630 536 moveto (Checker) [16.08 12 10.56 10.56 12 10.56 7.92] xshow @@ -1369,24 +1369,23 @@ end grestore end grestore % ProofChecker -> cic_proof_checking -newpath 218 526 moveto -226 512 238 496 254 488 curveto -268 480 378 482 393 480 curveto -404 478 415 476 426 474 curveto +newpath 653 526 moveto +643 511 630 496 613 488 curveto +589 476 409 493 360 483 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 427 477 moveto -436 472 lineto -426 471 lineto +newpath 362 480 moveto +351 480 lineto +359 486 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 427 477 moveto -436 472 lineto -426 471 lineto +newpath 362 480 moveto +351 480 lineto +359 486 lineto closepath stroke end grestore @@ -1396,22 +1395,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 632 846 moveto -546 846 lineto -546 810 lineto -632 810 lineto +newpath 658 846 moveto +572 846 lineto +572 810 lineto +658 810 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 632 846 moveto -546 846 lineto -546 810 lineto -632 810 lineto +newpath 658 846 moveto +572 846 lineto +572 810 lineto +658 810 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -553 820 moveto +579 820 moveto (Uwobo) [17.28 17.28 12 12 12] xshow @@ -1419,24 +1418,23 @@ end grestore end grestore % Uwobo -> content_pres -newpath 618 810 moveto -624 807 630 804 636 802 curveto -739 767 772 789 877 766 curveto -884 765 890 763 897 761 curveto +newpath 649 810 moveto +655 807 661 804 667 802 curveto +704 786 748 772 782 760 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 898 764 moveto -907 758 lineto -896 758 lineto +newpath 783 763 moveto +792 757 lineto +781 757 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 898 764 moveto -907 758 lineto -896 758 lineto +newpath 783 763 moveto +792 757 lineto +781 757 lineto closepath stroke end grestore @@ -1446,22 +1444,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 528 846 moveto -448 846 lineto -448 810 lineto -528 810 lineto +newpath 756 846 moveto +676 846 lineto +676 810 lineto +756 810 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 528 846 moveto -448 846 lineto -448 810 lineto -528 810 lineto +newpath 756 846 moveto +676 846 lineto +676 810 lineto +756 810 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -455 820 moveto +683 820 moveto (Whelp) [22.56 12 10.56 6.72 12] xshow @@ -1469,46 +1467,45 @@ end grestore end grestore % Whelp -> cic_disambiguation -newpath 520 810 moveto -526 807 531 804 537 802 curveto -580 785 628 770 669 760 curveto +newpath 743 810 moveto +749 807 754 804 760 802 curveto +835 773 858 782 935 766 curveto +944 764 954 762 963 759 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 670 763 moveto -679 758 lineto -669 757 lineto +newpath 964 762 moveto +973 757 lineto +963 756 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 670 763 moveto -679 758 lineto -669 757 lineto +newpath 964 762 moveto +973 757 lineto +963 756 lineto closepath stroke end grestore % Whelp -> content_pres -newpath 518 810 moveto -524 807 531 804 537 802 curveto -683 757 729 796 877 766 curveto -884 765 891 763 898 761 curveto +newpath 743 810 moveto +761 798 785 782 805 769 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 899 764 moveto -908 758 lineto -897 758 lineto +newpath 808 771 moveto +814 763 lineto +804 766 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 899 764 moveto -908 758 lineto -897 758 lineto +newpath 808 771 moveto +814 763 lineto +804 766 lineto closepath stroke end grestore diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 5e5bb5bef..d1cc2e54d 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -16,6 +16,7 @@ \newcommand{\AUTO}{\textsc{Auto}} \newcommand{\COQ}{Coq} \newcommand{\ELIM}{\textsc{Elim}} +\newcommand{\GDOME}{Gdome} \newcommand{\HELM}{Helm} \newcommand{\HINT}{\textsc{Hint}} \newcommand{\IN}{\ensuremath{\dN}} @@ -133,19 +134,19 @@ a a set of \emph{modules} also forming a DAG. Modules and libraries provide coherent sets of functionalities at different scales. Applications that require only a few functionalities -depend on a restricted set of libraries. \MATITA, our most complex -application, depends on every library. +depend on a restricted set of libraries. -Only the proof assistant \MATITA{} is an application meant to be used directly -by the user. All the other applications are Web services developed in the -HELM and MoWGLI projects and already described elsewhere. In particular: +Only the proof assistant \MATITA{} and the \WHELP{} search engine are +applications meant to be used directly by the user. All the other applications +are Web services developed in the HELM and MoWGLI projects and already described +elsewhere. In particular: \begin{itemize} \item The \emph{Getter} is a Web service to retrieve an (XML) document from a physical location (URL) given its logical name (URI). The Getter is responsible of updating a table that maps URIs to URLs. Thanks to the Getter it is possible to work on a logically monolithic library that is physically distributed on the network. More information on the Getter can be found - in~\cite{getter}. + in~\cite{zack-master}. \item \emph{Whelp} is a search engine to index and locate mathematical notions (axioms, theorems, definitions) in the logical library managed by the Getter. Typical examples of a query to Whelp are queries that search @@ -161,16 +162,16 @@ HELM and MoWGLI projects and already described elsewhere. In particular: two dimensional mathematical notation. Uwobo may also embed the rendering of mathematical notions into arbitrary documents before returning them. The Getter is used by Uwobo to retrieve the document to be rendered. - Uwobo has been described in~\cite{uwobo}. + Uwobo has been described in~\cite{zack-master}. \item The \emph{Proof Checker} is a Web service that, given the URI of notion in the distributed library, checks its correctness. Since the notion is likely to depend in an acyclic way over other notions, the proof checker is also responsible of building in a top-down way the DAG of all dependencies, checking in turn every notion for correctness. - The proof checker has been described in~\cite{proofchecker}. + The proof checker has been described in~\cite{zack-master}. \item The \emph{Dependency Analyzer} is a Web service that can produce a textual or graphical representation of the dependecies of an object. - The dependency analyzer has been described in~\cite{dependencyanalyzer}. + The dependency analyzer has been described in~\cite{zack-master}. \end{itemize} The dependency of a library or application over another library can @@ -188,10 +189,10 @@ library, we can focus on the representation of the mathematical information. \MATITA{} is based on (a variant of) the Calculus of (Co)Inductive Constructions (CIC). In CIC terms are used to represent mathematical expressions, types and proofs. \MATITA{} is able to handle terms at -four different levels of refinement. On each level it is possible to provide a -different set of functionalities. The four different levels are: -fully specified terms; partially specified terms; terms -at the content level; terms at the presentation level. +four different levels of specification. On each level it is possible to provide +a different set of functionalities. The four different levels are: +fully specified terms; partially specified terms; +content level terms; presentation level terms. \subsection{Fully specified terms} \emph{Fully specified terms} are CIC terms where no information is @@ -222,7 +223,7 @@ at the content level; terms at the presentation level. every time it needs to retrieve the definition of a mathematical notion referenced by a term that is being type-checked. - The Proof Checker is the Web service that provides an HTTP interface + The Proof Checker is the Web service that provides an interface to the \texttt{cic\_proof\_checking} library. We use metadata and a sort of crawler to index the mathematical notions @@ -270,7 +271,7 @@ the conversion check, the refiner is based on \emph{unification} that is a procedure that makes two partially specified term convertible by instantiating as few as possible metavariables that occur in them. -Since terms are use in CIC to represent proofs, so far correct incomplete +Since terms are used in CIC to represent proofs, correct incomplete proofs are represented by refinable partially specified terms. The metavariables that occur in the proof correspond to the conjectures still to be proved. The sequent associated to the metavariable is the conjecture the user needs to @@ -280,7 +281,8 @@ prove. proof. A tactic proves a conjecture possibly creating new (and hopefully simpler) conjectures. The implementation of tactics is given in the \texttt{tactics} library. It is heavily based on the refinement and unification -procedures of the \texttt{cic\_unification} library. +procedures of the \texttt{cic\_unification} library. \TODO{citare paramodulation +da qualche part o toglierla dal grafo} As fully specified terms, partially specified terms are not well suited for user consumption since their syntax is not extendible and it is not @@ -288,7 +290,7 @@ possible to adopt the usual mathematical notation. However they are already an improvement over fully specified terms since they allow to omit redundant information that can be inferred by the refiner. -\subsection{Terms at the content level} +\subsection{Content level terms} The language used to communicate proofs and expecially expressions with the user does not only needs to be extendible and accomodate the usual mathematical notation. It must also reflect the comfortable degree of imprecision and @@ -296,7 +298,7 @@ ambiguity that the mathematical language provides. For instance, it is common practice in mathematics to speak of a generic equality that can be used to compare any two terms. However, it is well known -that several equalities can be identified as soon as we care for decidability +that several equalities can be distinguished as soon as we care for decidability or for their computational properties. For instance equality over real numbers is well known to be undecidable, whereas it is decidable over rational numbers. @@ -314,7 +316,7 @@ practice to stick to the usual imprecise mathematical ontology. In the Mathematical Knowledge Management community this imprecise language is called the \emph{content level} representation of expressions. -In \MATITA{} we provide two translations from partially specified terms +In \MATITA{} we provide two translations: from partially specified terms to content level terms and the other way around. The first translation can also be applied to fully specified terms since a fully specified term is a special case of partially specified term where no metavariable or implicit term occurs. @@ -323,12 +325,13 @@ The translation from partially specified terms to content level terms must discriminate between terms used to represent proofs and terms used to represent expressions. The firsts are translated to a content level representation of proof steps that can easily be rendered in natural language. The latters -are translated to MathML Content formulae. MathML Content is a W3C standard +are translated to MathML Content formulae. MathML Content~\cite{mathml} is a W3C +standard for the representation of content level expressions in an XML extensible format. The translation to content level is implemented in the \texttt{acic\_content} library. Its input are \emph{annotated partially -specified terms}. Annotated partially specified terms are maximally unshared +specified terms}, that are maximally unshared partially specified terms enriched with additional typing information for each subterm. This information is used to discriminate between terms that represent proofs and terms that represent expressions. Part of it is also stored at the @@ -351,10 +354,10 @@ every ambiguous expression one partially specified term. The \texttt{disambiguation} library contains the implementation of the disambiguation algorithm we presented in \cite{disambiguation} that is responsible of building in an efficicent way the set of all ``correct'' -interpretations. An interpretation is correct if the partially refined term +interpretations. An interpretation is correct if the partially specified term obtained using the interpretation is refinable. -\subsection{Terms at the presentation level} +\subsection{Presentation level terms} Content level terms are a sort of abstract syntax trees for mathematical expressions and proofs. The concrete syntax given to these abstract trees @@ -368,7 +371,8 @@ single day, but they stick to a set of symbols that is more or less fixed. The fact that the presentation language is finite allows the definition of standard languages. In particular, for formulae we have adopt MathML -Presentation that is an XML dialect standardized by the W3C. To visually +Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To +visually represent proofs it is enough to embed formulae in plain text enriched with formatting boxes. Since the language of formatting boxes is very simple, many equivalent specifications exist and we have adopted our own, called @@ -378,21 +382,22 @@ The \texttt{content\_pres} library contains the implementation of the translation from content level terms to presentation level terms. The rendering of presentation level terms is left to the application that uses the library. However, in the \texttt{hgdome} library we provide a few -utility functions to build a GDOM MathML+BoxML tree from our presentation -level terms. GDOM MathML+BoxML trees can be rendered by the GtkMathView -widget developed by Luca Padovani \cite{gtkmathview}. The widget is +utility functions to build a \GDOME~\cite{gdome2} MathML+BoxML tree from our +presentation +level terms. \GDOME{} MathML+BoxML trees can be rendered by the GtkMathView +widget developed by Luca Padovani \cite{padovani}. The widget is particularly interesting since it allows to implement \emph{semantic selection}. Semantic selection is a technique that consists in enriching the presentation level terms with pointers to the content level terms and to the partially -refined terms they correspond to. Highlight of formulae in the widget is +specified terms they correspond to. Highlight of formulae in the widget is constrained to selection of meaningful expressions, i.e. expressions that -correspond to a lower level term. Once the rendering of a lower level term is +correspond to a lower\footnote{\TODO{non abbiamo parlato di ``ordine''}} level term. Once the rendering of a lower level term is selected it is possible for the application to retrieve the pointer to the lower level term. An example of applications of semantic selection is \emph{semantic cut\&paste}: the user can select an expression and paste it -elsewhere preserving its semantics (i.e. the partially enriched term), +elsewhere preserving its semantics (i.e. the partially specified term), possibly performing some semantic transformation over it (e.g. renaming variables that would be captured or lambda-lifting free variables). @@ -404,7 +409,7 @@ parsing library we have adopted (CamlP4) is not able to parse ambiguous grammars. Thus we require the mapping from presentation level terms (concrete syntax) to content level terms (abstract syntax) to be unique. This means that the user must fix once and for all the associativity and -precedence level of every operator is he using. In prctice this limitation +precedence level of every operator he is using. In prctice this limitation does not seem too strong. The reason is that the target of the translation is an ambiguous language and the user is free to associate to every content level term several different interpretations (as a @@ -421,7 +426,8 @@ providing a rendering service for the documents in the distributed library. To render a document given its URI, \UWOBO{} retrieves it using the \GETTER{} obtaining a document with fully specified terms. Then it translates it to the presentation level passing through the content level. Finally -it returns the result document to be rendered by the user's browser. +it returns the result document to be rendered by the user's +browser.\footnote{\TODO{manca la passata verso HTML}} \hrule -- 2.39.2