From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 24 Nov 2005 13:30:01 +0000 (+0000)
Subject: Da capo (matita2.tex).
X-Git-Tag: make_still_working~8117
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=22fae39d4d5da97fcd91d6c25158ffdaee9a6f86;p=helm.git

Da capo (matita2.tex).
---

diff --git a/helm/papers/matita/.cvsignore b/helm/papers/matita/.cvsignore
index 0964fd233..db408ffbb 100644
--- a/helm/papers/matita/.cvsignore
+++ b/helm/papers/matita/.cvsignore
@@ -4,3 +4,13 @@ matita.blg
 matita.dvi
 matita.log
 matita.out
+matita.ps
+matita.pdf
+matita2.aux
+matita2.bbl
+matita2.blg
+matita2.dvi
+matita2.log
+matita2.out
+matita2.ps
+matita2.pdf
diff --git a/helm/papers/matita/Makefile b/helm/papers/matita/Makefile
index d287d115c..dc95f6691 100644
--- a/helm/papers/matita/Makefile
+++ b/helm/papers/matita/Makefile
@@ -11,7 +11,7 @@
 ########################################################################
 
 # list of .tex _main_ files
-TEXS = matita.tex
+TEXS = matita2.tex
 
 # number of runs of latex (for table of contents, list of figures, ...)
 RUNS = 1
diff --git a/helm/papers/matita/libraries.ps b/helm/papers/matita/libraries.ps
new file mode 100644
index 000000000..2fe948119
--- /dev/null
+++ b/helm/papers/matita/libraries.ps
@@ -0,0 +1,953 @@
+%!PS-Adobe-2.0
+%%Creator: dot version 2.2.1 (Tue Apr 12 00:03:35 UTC 2005)
+%%For: (sacerdot) Claudio Sacerdoti Coen,,,
+%%Title: G
+%%Pages: (atend)
+%%BoundingBox: 35 35 461 649
+%%EndComments
+save
+%%BeginProlog
+/DotDict 200 dict def
+DotDict begin
+
+/setupLatin1 {
+mark
+/EncodingVector 256 array def
+ EncodingVector 0
+
+ISOLatin1Encoding 0 255 getinterval putinterval
+
+EncodingVector
+  dup 306 /AE
+  dup 301 /Aacute
+  dup 302 /Acircumflex
+  dup 304 /Adieresis
+  dup 300 /Agrave
+  dup 305 /Aring
+  dup 303 /Atilde
+  dup 307 /Ccedilla
+  dup 311 /Eacute
+  dup 312 /Ecircumflex
+  dup 313 /Edieresis
+  dup 310 /Egrave
+  dup 315 /Iacute
+  dup 316 /Icircumflex
+  dup 317 /Idieresis
+  dup 314 /Igrave
+  dup 334 /Udieresis
+  dup 335 /Yacute
+  dup 376 /thorn
+  dup 337 /germandbls
+  dup 341 /aacute
+  dup 342 /acircumflex
+  dup 344 /adieresis
+  dup 346 /ae
+  dup 340 /agrave
+  dup 345 /aring
+  dup 347 /ccedilla
+  dup 351 /eacute
+  dup 352 /ecircumflex
+  dup 353 /edieresis
+  dup 350 /egrave
+  dup 355 /iacute
+  dup 356 /icircumflex
+  dup 357 /idieresis
+  dup 354 /igrave
+  dup 360 /dcroat
+  dup 361 /ntilde
+  dup 363 /oacute
+  dup 364 /ocircumflex
+  dup 366 /odieresis
+  dup 362 /ograve
+  dup 365 /otilde
+  dup 370 /oslash
+  dup 372 /uacute
+  dup 373 /ucircumflex
+  dup 374 /udieresis
+  dup 371 /ugrave
+  dup 375 /yacute
+  dup 377 /ydieresis  
+
+% Set up ISO Latin 1 character encoding
+/starnetISO {
+        dup dup findfont dup length dict begin
+        { 1 index /FID ne { def }{ pop pop } ifelse
+        } forall
+        /Encoding EncodingVector def
+        currentdict end definefont
+} def
+/Times-Roman starnetISO def
+/Times-Italic starnetISO def
+/Times-Bold starnetISO def
+/Times-BoldItalic starnetISO def
+/Helvetica starnetISO def
+/Helvetica-Oblique starnetISO def
+/Helvetica-Bold starnetISO def
+/Helvetica-BoldOblique starnetISO def
+/Courier starnetISO def
+/Courier-Oblique starnetISO def
+/Courier-Bold starnetISO def
+/Courier-BoldOblique starnetISO def
+cleartomark
+} bind def
+
+%%BeginResource: procset graphviz 0 0
+/coord-font-family /Times-Roman def
+/default-font-family /Times-Roman def
+/coordfont coord-font-family findfont 8 scalefont def
+
+/InvScaleFactor 1.0 def
+/set_scale {
+	dup 1 exch div /InvScaleFactor exch def
+	dup scale
+} bind def
+
+% styles
+/solid { [] 0 setdash } bind def
+/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
+/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
+/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
+/bold { 2 setlinewidth } bind def
+/filled { } bind def
+/unfilled { } bind def
+/rounded { } bind def
+/diagonals { } bind def
+
+% hooks for setting color 
+/nodecolor { sethsbcolor } bind def
+/edgecolor { sethsbcolor } bind def
+/graphcolor { sethsbcolor } bind def
+/nopcolor {pop pop pop} bind def
+
+/beginpage {	% i j npages
+	/npages exch def
+	/j exch def
+	/i exch def
+	/str 10 string def
+	npages 1 gt {
+		gsave
+			coordfont setfont
+			0 0 moveto
+			(\() show i str cvs show (,) show j str cvs show (\)) show
+		grestore
+	} if
+} bind def
+
+/set_font {
+	findfont exch
+	scalefont setfont
+} def
+
+% draw aligned label in bounding box aligned to current point
+/alignedtext {			% width adj text
+	/text exch def
+	/adj exch def
+	/width exch def
+	gsave
+		width 0 gt {
+			text stringwidth pop adj mul 0 rmoveto
+		} if
+		[] 0 setdash
+		text show
+	grestore
+} def
+
+/boxprim {				% xcorner ycorner xsize ysize
+		4 2 roll
+		moveto
+		2 copy
+		exch 0 rlineto
+		0 exch rlineto
+		pop neg 0 rlineto
+		closepath
+} bind def
+
+/ellipse_path {
+	/ry exch def
+	/rx exch def
+	/y exch def
+	/x exch def
+	matrix currentmatrix
+	newpath
+	x y translate
+	rx ry scale
+	0 0 1 0 360 arc
+	setmatrix
+} bind def
+
+/endpage { showpage } bind def
+/showpage { } def
+
+/layercolorseq
+	[	% layer color sequence - darkest to lightest
+		[0 0 0]
+		[.2 .8 .8]
+		[.4 .8 .8]
+		[.6 .8 .8]
+		[.8 .8 .8]
+	]
+def
+
+/layerlen layercolorseq length def
+
+/setlayer {/maxlayer exch def /curlayer exch def
+	layercolorseq curlayer 1 sub layerlen mod get
+	aload pop sethsbcolor
+	/nodecolor {nopcolor} def
+	/edgecolor {nopcolor} def
+	/graphcolor {nopcolor} def
+} bind def
+
+/onlayer { curlayer ne {invis} if } def
+
+/onlayers {
+	/myupper exch def
+	/mylower exch def
+	curlayer mylower lt
+	curlayer myupper gt
+	or
+	{invis} if
+} def
+
+/curlayer 0 def
+
+%%EndResource
+%%EndProlog
+%%BeginSetup
+14 default-font-family set_font
+1 setmiterlimit
+% /arrowlength 10 def
+% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+    userdict (<<) cvn ([) cvn load put
+    userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndSetup
+%%Page: 1 1
+%%PageBoundingBox: 36 36 461 649
+%%PageOrientation: Portrait
+gsave
+35 35 426 614 boxprim clip newpath
+36 36 translate
+0 0 1 beginpage
+0 0 translate 0 rotate
+0.000 0.000 0.000 graphcolor
+14.00 /Times-Roman set_font
+
+%	paramodulation
+gsave 10 dict begin
+164 594 57 18 ellipse_path
+stroke
+gsave 10 dict begin
+119 589 moveto
+(paramodulation)
+[6.96 6.24 4.56 6.24 10.8 6.96 6.96 6.96 3.84 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	cic_disambiguation
+gsave 10 dict begin
+164 522 68 18 ellipse_path
+stroke
+gsave 10 dict begin
+109 517 moveto
+(cic_disambiguation)
+[6.24 3.84 6.24 6.96 6.96 3.84 5.52 6.24 10.8 6.96 3.84 6.96 6.96 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	paramodulation -> cic_disambiguation
+newpath 164 576 moveto
+164 568 164 559 164 550 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 168 550 moveto
+164 540 lineto
+161 550 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 168 550 moveto
+164 540 lineto
+161 550 lineto
+closepath
+stroke
+end grestore
+
+%	cic_notation
+gsave 10 dict begin
+48 378 48 18 ellipse_path
+stroke
+gsave 10 dict begin
+13 373 moveto
+(cic_notation)
+[6.24 3.84 6.24 6.96 6.96 6.96 3.84 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	cic_disambiguation -> cic_notation
+newpath 128 507 moveto
+111 498 91 485 77 468 curveto
+64 450 56 425 52 406 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 55 405 moveto
+50 396 lineto
+49 406 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 55 405 moveto
+50 396 lineto
+49 406 lineto
+closepath
+stroke
+end grestore
+
+%	tactics
+gsave 10 dict begin
+275 450 31 18 ellipse_path
+stroke
+gsave 10 dict begin
+256 445 moveto
+(tactics)
+[3.84 6.24 6.24 3.84 3.84 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+%	cic_disambiguation -> tactics
+newpath 190 505 moveto
+207 494 228 480 246 469 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 248 472 moveto
+254 463 lineto
+244 466 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 248 472 moveto
+254 463 lineto
+244 466 lineto
+closepath
+stroke
+end grestore
+
+%	cic_proof_checking
+gsave 10 dict begin
+242 306 68 18 ellipse_path
+stroke
+gsave 10 dict begin
+186 301 moveto
+(cic_proof_checking)
+[6.24 3.84 6.24 6.96 6.96 4.56 6.96 6.96 4.56 6.96 6.24 6.96 6.24 6.24 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	cic_notation -> cic_proof_checking
+newpath 82 365 moveto
+113 354 158 337 192 325 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 194 328 moveto
+202 321 lineto
+191 321 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 194 328 moveto
+202 321 lineto
+191 321 lineto
+closepath
+stroke
+end grestore
+
+%	utf8_macros
+gsave 10 dict begin
+48 306 48 18 ellipse_path
+stroke
+gsave 10 dict begin
+12 301 moveto
+(utf8_macros)
+[6.96 3.84 4.56 6.96 6.96 10.8 6.24 6.24 4.56 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+%	cic_notation -> utf8_macros
+newpath 48 360 moveto
+48 352 48 343 48 334 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 52 334 moveto
+48 324 lineto
+45 334 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 52 334 moveto
+48 324 lineto
+45 334 lineto
+closepath
+stroke
+end grestore
+
+%	metadata
+gsave 10 dict begin
+386 378 38 18 ellipse_path
+stroke
+gsave 10 dict begin
+360 373 moveto
+(metadata)
+[10.8 6.24 3.84 6.24 6.96 6.24 3.84 6.24]
+xshow
+end grestore
+end grestore
+
+%	tactics -> metadata
+newpath 296 436 moveto
+312 426 336 411 355 399 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 357 402 moveto
+363 393 lineto
+353 396 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 357 402 moveto
+363 393 lineto
+353 396 lineto
+closepath
+stroke
+end grestore
+
+%	cic_unification
+gsave 10 dict begin
+275 378 55 18 ellipse_path
+stroke
+gsave 10 dict begin
+233 373 moveto
+(cic_unification)
+[6.24 3.84 6.24 6.96 6.96 6.96 3.84 4.56 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	tactics -> cic_unification
+newpath 275 432 moveto
+275 424 275 415 275 406 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 279 406 moveto
+275 396 lineto
+272 406 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 279 406 moveto
+275 396 lineto
+272 406 lineto
+closepath
+stroke
+end grestore
+
+%	cic_transformations
+gsave 10 dict begin
+154 450 68 18 ellipse_path
+stroke
+gsave 10 dict begin
+98 445 moveto
+(cic_transformations)
+[6.24 3.84 6.24 6.96 3.84 4.56 6.24 6.96 5.52 4.56 6.96 4.56 10.8 6.24 3.84 3.84 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+%	cic_transformations -> cic_notation
+newpath 129 433 moveto
+115 423 95 410 79 399 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 81 396 moveto
+71 394 lineto
+78 402 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 81 396 moveto
+71 394 lineto
+78 402 lineto
+closepath
+stroke
+end grestore
+
+%	cic_omdoc
+gsave 10 dict begin
+158 378 44 18 ellipse_path
+stroke
+gsave 10 dict begin
+127 373 moveto
+(cic_omdoc)
+[6.24 3.84 6.24 6.96 6.96 10.8 6.96 6.96 6.24]
+xshow
+end grestore
+end grestore
+
+%	cic_transformations -> cic_omdoc
+newpath 155 432 moveto
+156 424 156 415 156 406 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 159 406 moveto
+157 396 lineto
+153 406 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 159 406 moveto
+157 396 lineto
+153 406 lineto
+closepath
+stroke
+end grestore
+
+%	cic_omdoc -> cic_proof_checking
+newpath 177 362 moveto
+188 352 202 340 214 330 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 217 332 moveto
+222 323 lineto
+212 327 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 217 332 moveto
+222 323 lineto
+212 327 lineto
+closepath
+stroke
+end grestore
+
+%	getter
+gsave 10 dict begin
+292 234 29 18 ellipse_path
+stroke
+gsave 10 dict begin
+276 229 moveto
+(getter)
+[6.96 6.24 3.84 3.84 6.24 4.56]
+xshow
+end grestore
+end grestore
+
+%	cic_proof_checking -> getter
+newpath 254 288 moveto
+260 280 267 269 274 259 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 277 261 moveto
+280 251 lineto
+271 257 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 277 261 moveto
+280 251 lineto
+271 257 lineto
+closepath
+stroke
+end grestore
+
+%	cic
+gsave 10 dict begin
+208 234 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+199 229 moveto
+(cic)
+[6.24 3.84 6.24]
+xshow
+end grestore
+end grestore
+
+%	cic_proof_checking -> cic
+newpath 233 288 moveto
+229 280 225 270 220 261 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 223 260 moveto
+216 252 lineto
+217 263 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 223 260 moveto
+216 252 lineto
+217 263 lineto
+closepath
+stroke
+end grestore
+
+%	metadata -> cic_proof_checking
+newpath 360 365 moveto
+339 354 308 339 283 327 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 284 324 moveto
+274 322 lineto
+281 330 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 284 324 moveto
+274 322 lineto
+281 330 lineto
+closepath
+stroke
+end grestore
+
+%	hmysql
+gsave 10 dict begin
+386 234 34 18 ellipse_path
+stroke
+gsave 10 dict begin
+364 229 moveto
+(hmysql)
+[6.96 10.8 6.96 5.52 6.96 3.84]
+xshow
+end grestore
+end grestore
+
+%	metadata -> hmysql
+newpath 386 360 moveto
+386 335 386 291 386 262 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 390 262 moveto
+386 252 lineto
+383 262 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 390 262 moveto
+386 252 lineto
+383 262 lineto
+closepath
+stroke
+end grestore
+
+%	cic_unification -> cic_proof_checking
+newpath 267 360 moveto
+263 352 259 342 254 333 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 257 332 moveto
+250 324 lineto
+251 335 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 257 332 moveto
+250 324 lineto
+251 335 lineto
+closepath
+stroke
+end grestore
+
+%	registry
+gsave 10 dict begin
+386 162 35 18 ellipse_path
+stroke
+gsave 10 dict begin
+364 157 moveto
+(registry)
+[4.56 6.24 6.96 3.84 5.52 3.84 4.56 6.96]
+xshow
+end grestore
+end grestore
+
+%	hmysql -> registry
+newpath 386 216 moveto
+386 208 386 199 386 190 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 390 190 moveto
+386 180 lineto
+383 190 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 390 190 moveto
+386 180 lineto
+383 190 lineto
+closepath
+stroke
+end grestore
+
+%	urimanager
+gsave 10 dict begin
+208 162 45 18 ellipse_path
+stroke
+gsave 10 dict begin
+175 157 moveto
+(urimanager)
+[6.96 4.56 3.84 10.8 6.24 6.96 6.24 6.96 6.24 4.56]
+xshow
+end grestore
+end grestore
+
+%	getter -> urimanager
+newpath 275 219 moveto
+263 209 248 196 235 185 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 237 182 moveto
+227 178 lineto
+232 187 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 237 182 moveto
+227 178 lineto
+232 187 lineto
+closepath
+stroke
+end grestore
+
+%	getter -> registry
+newpath 311 220 moveto
+325 210 343 195 359 183 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 361 186 moveto
+367 177 lineto
+357 180 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 361 186 moveto
+367 177 lineto
+357 180 lineto
+closepath
+stroke
+end grestore
+
+%	logger
+gsave 10 dict begin
+302 162 31 18 ellipse_path
+stroke
+gsave 10 dict begin
+284 157 moveto
+(logger)
+[3.84 6.96 6.96 6.96 6.24 4.56]
+xshow
+end grestore
+end grestore
+
+%	getter -> logger
+newpath 295 216 moveto
+296 208 297 199 298 190 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 301 190 moveto
+299 180 lineto
+295 190 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 301 190 moveto
+299 180 lineto
+295 190 lineto
+closepath
+stroke
+end grestore
+
+%	xml
+gsave 10 dict begin
+260 90 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+248 85 moveto
+(xml)
+[6.96 10.8 3.84]
+xshow
+end grestore
+end grestore
+
+%	cic -> xml
+newpath 189 221 moveto
+176 212 161 197 154 180 curveto
+147 165 145 157 154 144 curveto
+169 119 199 105 224 98 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 225 101 moveto
+234 95 lineto
+223 95 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 225 101 moveto
+234 95 lineto
+223 95 lineto
+closepath
+stroke
+end grestore
+
+%	cic -> urimanager
+newpath 208 216 moveto
+208 208 208 199 208 190 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 212 190 moveto
+208 180 lineto
+205 190 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 212 190 moveto
+208 180 lineto
+205 190 lineto
+closepath
+stroke
+end grestore
+
+%	extlib
+gsave 10 dict begin
+260 18 29 18 ellipse_path
+stroke
+gsave 10 dict begin
+244 13 moveto
+(extlib)
+[6.24 6.96 3.84 3.84 3.84 6.96]
+xshow
+end grestore
+end grestore
+
+%	xml -> extlib
+newpath 260 72 moveto
+260 64 260 55 260 46 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 264 46 moveto
+260 36 lineto
+257 46 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 264 46 moveto
+260 36 lineto
+257 46 lineto
+closepath
+stroke
+end grestore
+
+%	registry -> xml
+newpath 362 148 moveto
+342 137 312 120 290 107 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 291 104 moveto
+281 102 lineto
+288 110 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 291 104 moveto
+281 102 lineto
+288 110 lineto
+closepath
+stroke
+end grestore
+endpage
+showpage
+grestore
+%%PageTrailer
+%%EndPage: 1
+%%Trailer
+%%Pages: 1
+end
+restore
+%%EOF
diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
new file mode 100644
index 000000000..7cfdde2e9
--- /dev/null
+++ b/helm/papers/matita/matita2.tex
@@ -0,0 +1,324 @@
+\documentclass{kluwer}
+\usepackage{color}
+\usepackage{graphicx}
+% \usepackage{amssymb,amsmath}
+\usepackage{hyperref}
+% \usepackage{picins}
+\usepackage{color}
+\usepackage{fancyvrb}
+\usepackage[show]{ed}
+
+\definecolor{gray}{gray}{0.85}
+%\newcommand{\logo}[3]{
+%\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
+%}
+
+\newcommand{\AUTO}{\textsc{Auto}}
+\newcommand{\COQ}{Coq}
+\newcommand{\ELIM}{\textsc{Elim}}
+\newcommand{\HELM}{Helm}
+\newcommand{\HINT}{\textsc{Hint}}
+\newcommand{\IN}{\ensuremath{\dN}}
+\newcommand{\INSTANCE}{\textsc{Instance}}
+\newcommand{\IR}{\ensuremath{\dR}}
+\newcommand{\IZ}{\ensuremath{\dZ}}
+\newcommand{\LIBXSLT}{LibXSLT}
+\newcommand{\LOCATE}{\textsc{Locate}}
+\newcommand{\MATCH}{\textsc{Match}}
+\newcommand{\MATITA}{Matita}
+\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
+\newcommand{\MOWGLI}{MoWGLI}
+\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
+\newcommand{\NATIND}{\mathit{nat\_ind}}
+\newcommand{\NUPRL}{NuPRL}
+\newcommand{\OCAML}{OCaml}
+\newcommand{\PROP}{\mathit{Prop}}
+\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
+\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
+\newcommand{\UWOBO}{UWOBO}
+\newcommand{\WHELP}{Whelp}
+\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
+\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
+\newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
+\newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
+\newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
+\newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
+\newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
+\newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
+\newcommand{\SKIP}{\MATHTT{skip}}
+\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
+
+\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
+\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
+\newcommand{\URI}[1]{\texttt{#1}}
+
+%{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
+\newenvironment{grafite}{\VerbatimEnvironment
+ \begin{SaveVerbatim}{boxtmp}}%
+ {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
+  \begin{center}
+   \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
+  \end{center}}
+
+\newcounter{example}
+\newenvironment{example}{\stepcounter{example}\vspace{0.5em}\noindent\emph{Example} \arabic{example}.}
+ {}
+\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
+\newcommand{\FILE}[1]{\texttt{#1}}
+% \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}}
+\newcommand{\NOTE}[1]{\ednote{#1}{foo}}
+\newcommand{\TODO}[1]{\textbf{TODO: #1}}
+
+\newsavebox{\tmpxyz}
+\newcommand{\sequent}[2]{
+  \savebox{\tmpxyz}[0.9\linewidth]{
+    \begin{minipage}{0.9\linewidth}
+      \ensuremath{#1} \\
+      \rule{3cm}{0.03cm}\\
+      \ensuremath{#2}
+    \end{minipage}}\setlength{\fboxsep}{3mm}%
+  \begin{center}
+   \fcolorbox{black}{gray}{\usebox{\tmpxyz}}
+  \end{center}}
+
+\bibliographystyle{plain}
+
+\begin{document}
+
+\begin{opening}
+
+ \title{The \MATITA{} Proof Assistant}
+
+\author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
+\author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
+\author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
+\author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
+\institute{Department of Computer Science, University of Bologna\\
+ Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
+
+\runningtitle{The Matita proof assistant}
+\runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
+
+% \date{data}
+
+\begin{motto}
+``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
+\end{motto}
+
+\begin{abstract}
+ abstract qui
+\end{abstract}
+
+\keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
+Digital Libraries}
+
+\end{opening}
+
+\begin{figure}[t]
+ \begin{center}
+  \includegraphics[width=0.9\textwidth]{libraries}
+  \caption{\MATITA{} libraries}
+ \end{center}
+ \label{fig:libraries}
+\end{figure}
+
+\section{Overview of the Architecture}
+Fig.~\ref{fig:libraries} shows the architecture of the \emph{libraries} (circle nodes)
+and \emph{applications} (squared nodes) developed in the HELM project.
+
+Applications and libraries depend over other libraries forming a
+directed acyclic graph (DAG). Each library can be decomposed in
+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.
+
+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:
+\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}.
+ \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
+   for a theorem that generalize or instantiate a given formula, or that
+   can be immediately applied to prove a given goal. The output of Whelp is
+   an XML document that lists the URIs of a complete set of candidates that
+   are likely to satisfy the given query. The set is complete in the sense
+   that no notion that actually satisfies the query is thrown away. However,
+   the query is only approssimated in the sense that false matches can be
+   returned. Whelp has been described in~\cite{whelp}.
+ \item \emph{Uwobo} is a Web service that, given the URI of a mathematical
+   notion in the distributed library, renders it according to the user provided
+   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}.
+ \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}.
+ \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}.
+\end{itemize}
+
+The dependency of a library or application over another library can
+be satisfied by linking the library in the same executable.
+For those libraries whose functionalities are also provided by the
+aforementioned Web services, it is also possible to link stub code that
+forwards the request to a remote Web service. For instance, the Getter
+is just a wrapper to the \texttt{getter} library that allows the library
+to be used as a Web service. \MATITA{} can directly link the code of the
+\texttt{getter} library, or it can use a stub library with the same API
+that forwards every request to the Getter.
+
+To better understand the architecture of \MATITA{} and the role of each
+library, we can focus on the rappresentation 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.
+
+\subsection{Fully specified terms}
+ \emph{Fully specified terms} are CIC terms where no information is
+   missing or left implicit. A fully specified term should be well-typed.
+   The mathematical notions (axioms, definitions, theorems) that are stored
+   in our mathematical library are fully specified and well-typed terms.
+   Fully specified terms are extremely verbose (to make type-checking
+   decidable). Their syntax is fixed and does not resemble the usual
+   extendible mathematical notation. They are not meant for direct user
+   consumption.
+
+   The \texttt{cic} library defines the data type that represents CIC terms
+   and provides a parser for terms stored in an XML format.
+
+   The most important library that deals with fully specified terms is
+   \texttt{cic\_proof\_checking}. It implements the procedure that verifies
+   if a fully specified term is well-typed. It also implements the
+   \emph{conversion} judgement that verifies if two given terms are
+   computationally equivalent (i.e. they share the same normal form).
+
+   Terms may reference other mathematical notions in the library.
+   One commitment of our project is that the library should be physically
+   distributed. The \texttt{getter} library manages the distribution,
+   providing a mapping from logical names (URIs) to the physical location
+   of a notion (an URL). The \texttt{urimanager} library provides the URI
+   data type and several utility functions over URIs. The
+   \texttt{cic\_proof\_checking} library calls the \texttt{getter} library
+   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
+   to the \texttt{cic\_proof\_checking} library.
+
+   We use metadata and a sort of crawler to index the mathematical notions
+   in the distributed library. We are interested in retrieving a notion
+   by matching, instantiation or generalization of a user or system provided
+   mathematical expression. Thus we need to collect metadata over the fully
+   specified terms and to store the metadata in some kind of (relational)
+   database for later usage. The \texttt{hmysql} library provides a simplified
+   interface to a (possibly remote) MySql database system used to store the
+   metadata. The \texttt{metadata} library defines the data type of the metadata
+   we are collecting and the functions that extracts the metadata from the
+   mathematical notions (the main functionality of the crawler).
+   The \texttt{whelp} library implements a search engine that performs
+   approximated queries by matching/instantiation/generalization. The queries
+   operate only on the metadata and do not involve any actual matching
+   (that will be described later on and that is implemented in the
+    \texttt{cic\_unification} library). Not performing any actual matching
+   the query only returns a complete and hopefully small set of matching
+   candidates. The process that has issued the query is responsible of
+   actually retrieving from the distributed library the candidates to prune
+   out false matches if interested in doing so.
+
+   The Whelp search engine is the Web service that provides an interface to
+   the \texttt{whelp} library.
+
+\subsection{Partially specified terms}
+\emph{Partially specified terms} are CIC terms where subterms can be omitted.
+Omitted subterms can bear no information at all or they may be associated to
+a sequent. The formers are called \emph{implicit terms} and they occur only
+linearly. The latters may occur multiple times and are called
+\emph{metavariables}. An \emph{explicit substitution} is applied to each
+occurrence of a metavariable. A metavariable stand for a term whose type is
+given by the conclusion of the sequent. The term must be closed in the
+context that is given by the ordered list of hypotheses of the sequent.
+The explicit substitution instantiates every hypothesis with an actual
+value for the term bound by the hypothesis.
+
+Partially specified terms are not required to be well-typed. However a
+partially specified term should be \emph{refinable}. A \emph{refiner} is
+a type-inference procedure that can instantiate implicit terms and
+metavariables and that can introduce \emph{implicit coercions} to make a
+partially specified term be well-typed. The refiner of \MATITA{} is implemented
+in the \texttt{cic\_unification} library. As the type checker is based on
+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
+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
+prove.
+
+\emph{Tactics} are the procedures that the user can apply to progress in the
+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.
+
+As fully specified terms, partially specified terms are not well suited
+for user consumption since their syntax is not extendible and it is not
+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{Terms at the presentation level}
+
+\hrule
+
+At the bottom of the DAG we have a few libraries (\texttt{extlib},
+\texttt{xml} and the \texttt{registry}) that provide a core of
+useful functions used everywhere else. In particular, the \texttt{xml} library
+to easily represent, parse and pretty-print XML files is a central component
+since in HELM every piece of information is stored in \ldots. [FINIRE]
+The other basic libraries provide often needed operations over generic
+data structures (\texttt{extlib}) and central storage for configuration options
+(the \texttt{registry}).
+
+\texttt{urimanager}
+
+\texttt{getter}
+
+\texttt{cic}
+
+\acknowledgements
+We would like to thank all the students that during the past
+five years collaborated in the \HELM{} project and contributed to 
+the development of Matita, and in particular
+A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi, 
+V.Tamburrelli.
+
+\theendnotes
+
+\bibliography{matita}
+
+
+\end{document}
+