From 552dbd63f202c8876605b62621c3e727d71e3963 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 14 Apr 2004 17:33:12 +0000
Subject: [PATCH] updating all sections

---
 helm/mathql/doc/fguidi-defs.sty               |  121 --
 helm/mathql/doc/llncs.cls                     | 1189 +++++++++++++++++
 helm/mathql/doc/mathql.tex                    |   23 +-
 helm/mathql/doc/mathql_bib.tex                |    1 -
 helm/mathql/doc/mathql_introduction.tex       |   16 +-
 .../mathql/doc/mathql_introduction_avsets.tex |  153 +--
 helm/mathql/doc/mathql_introduction_basic.tex |  136 ++
 helm/mathql/doc/mathql_introduction_core.tex  |  120 +-
 .../doc/mathql_introduction_property.tex      |  132 +-
 .../doc/mathql_introduction_textual.tex       |  109 +-
 helm/mathql/doc/mathql_macros.sty             |  118 +-
 helm/mathql/doc/mathql_operational.tex        |    6 +-
 .../doc/mathql_operational_background.tex     |   38 +-
 helm/mathql/doc/mathql_operational_basic.tex  |  298 +++++
 helm/mathql/doc/mathql_operational_core.tex   |  212 ++-
 helm/mathql/doc/mathql_overview.tex           |   15 +-
 helm/mathql/doc/mathql_tests.tex              |   28 +
 17 files changed, 2111 insertions(+), 604 deletions(-)
 delete mode 100644 helm/mathql/doc/fguidi-defs.sty
 create mode 100644 helm/mathql/doc/llncs.cls
 create mode 100644 helm/mathql/doc/mathql_introduction_basic.tex
 create mode 100644 helm/mathql/doc/mathql_operational_basic.tex
 create mode 100644 helm/mathql/doc/mathql_tests.tex

diff --git a/helm/mathql/doc/fguidi-defs.sty b/helm/mathql/doc/fguidi-defs.sty
deleted file mode 100644
index df71b4470..000000000
--- a/helm/mathql/doc/fguidi-defs.sty
+++ /dev/null
@@ -1,121 +0,0 @@
-%\DeclareSymbolFont{stmary}{U}{stmary}{m}{n}
-%\DeclareFontFamily{U}{stmary}{}%
-%\DeclareFontShape{U}{stmary}{m}{n}{<-6>stmary5<6-8>stmary7<8->stmary10}{}%
-%\DeclareMathSymbol{\odb}{\mathopen}{stmary}{"4A}
-%\DeclareMathSymbol{\cdb}{\mathclose}{stmary}{"4B}
-
-\usepackage{amssymb}
-\usepackage{stmaryrd}
-
-% LOGIC  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-
-% utilities
-
-\def\cv{\,]}
-\def\ov{[\,}
-\def\spc{\hspace{1em}} % 0.25em per la tesi
-\def\nop{{}}
-\def\Nop{\noindent\hbox to 0pt{\vbox to 1ex{\vfil}\hfil}}
-\def\gdlap#1#2{\vbox to 0pt {\vskip#2\hbox{#1}\vss}}
-\def\?#1{\mathord{#1}}
-
-% inference trees
-
-\def\imain#1{{\offinterlineskip\lineskip=2pt\noindent
-  \hbox{$\vcenter{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}
-\def\itree#1{{\offinterlineskip\lineskip=2pt\noindent
-  \hbox{$\vbox{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}
-
-\def\setnames@#1#2{&\gdlap{\kern2pt$#1$}{#2}} 
-\def\iname#1 {\cr\hrulefill\setnames@{#1}{-1.0ex}\cr}
-\def\inames#1 {\cr\hrulefill\cr\hrulefill\setnames@{#1}{-1.2ex}\cr}
-\def\ivrule{\cr\vrule height 3ex \cr}
-\def\discharge#1#2 {\iname{#1\,#2} }
-\def\assume#1#2{\ov #1\cv\rlap{$^{#2}$}}
-
-% single rules
-
-\def\irule#1#2#3{\imain{#1 \iname{#2} #3 }}   % "single step"
-\def\irules#1#2#3{\imain{#1 \inames{#2} #3 }} % "multistep"
-
-\def\drule#1#2#3{\itree{#1 \iname{#2} #3 }}   % "single step"
-\def\drules#1#2#3{\itree{#1 \inames{#2} #3 }} % "multistep"
-
-\def\cirule#1#2#3{$\vcenter{\irule{#1}{#2}{#3}}$}   % "single step"
-\def\cirules#1#2#3{$\vcenter{\irules{#1}{#2}{#3}}$} % "multistep"
-
-% MATHEMATICS  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\def\a{\phi}
-\def\b{\psi}
-\def\c{\xi}
-\def\d{\eta}
-\def\A{\Phi}
-\def\B{\Psi}
-\def\C{\Xi}
-\def\jolly{\mathbin\square}
-\def\lall{\forall}
-\def\lex{\exists}
-\def\lbot{{\bot}}
-\def\lexcl{\mathrel\leftarrow}
-\def\limp{\mathrel\rightarrow}
-\def\liff{\mathrel\leftrightarrow}
-\def\lone{1}
-\def\lplus{\mathrel\oplus}
-\def\ltimes{\mathrel\otimes}
-\def\ltop{{\top}}
-\def\lzero{0}
-\def\lpar{\mathrel\bindnasrepma}
-\def\lamp{\mathrel\binampersand}
-
-\def\meet{\between}
-\def\bigsor{\bigcup}
-\def\bigsand{\bigcap}
-\def\sand{\cap}
-\def\sdor{\sqcup}
-\def\sor{\cup}
-\def\simp{\Rightarrow}
-\def\snot{-}
-\def\sub{\subseteq}
-\def\sup{\supseteq}
-\def\sbot{\emptyset}
-\def\stop{\ltop}
-
-\def\after{\mathbin\circ}
-\def\app{\mathbin @}
-\def\e{\mathrel\epsilon}
-\def\oft{\mathrel :}
-\def\p{{^\prime}}
-\def\st{\mathrel |}
-\def\subset#1{\{#1\}}
-\def\yld{\mathrel\vdash}
-\def\Frm{\textsf{Frm}}
-\def\Trm{\textsf{Trm}}
-\def\LB{{\bf B}}
-\def\LBm{{\bf B}$^-$}
-\def\LBmi{{\bf B}$^-_{\limp}$}
-\def\LBmiq{{\bf B}$^-_{\limp\lexcl\lall\lex}$}
-\def\LBLS{{\bf BLS}}
-\def\P{{\cal P}}
-
-\def\mand{\mathrel{\textbf{and}}}
-\def\miff{\mathrel{\textbf{iff}}}
-\def\mimp{\mathrel{\textbf{implies}}}
-\def\mpiff{\mathrel{\textbf{\frenchspacing prim. iff}}}
-\def\mpimp{\mathrel{\textbf{\frenchspacing prim. implies}}}
-\def\mtrue{\mathord{\textbf{true}}}
-\def\mall{\mathrel{\textbf{all}}}
-
-% TEXT  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\def\EM#1{\noindent\hbox{\frenchspacing\em #1}}
-\def\TT#1{\noindent\hbox{\frenchspacing\tt #1}}
-\def\RM#1{\noindent\hbox{\frenchspacing\rm #1}}
-\def\URI#1{\texttt{<#1>}}
-
-\def\ie{{\frenchspacing i.e.}}
-\def\df#1{{\bf #1}}
-\long\def\xcomment#1{}
-\def\proc{{\frenchspacing proc.}}
-\def\etc{{\frenchspacing etc.}}
-\def\po{{\frenchspacing p.o.}}
diff --git a/helm/mathql/doc/llncs.cls b/helm/mathql/doc/llncs.cls
new file mode 100644
index 000000000..29e505e60
--- /dev/null
+++ b/helm/mathql/doc/llncs.cls
@@ -0,0 +1,1189 @@
+% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002)
+% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
+%
+%%
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+%%
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{llncs}[2002/01/28 v2.13
+^^J LaTeX document class for Lecture Notes in Computer Science]
+% Options
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
+\DeclareOption{oribibl}{\let\oribibl=Y}
+\let\if@custvec\iftrue
+\DeclareOption{orivec}{\let\if@custvec\iffalse}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+
+\let\if@openbib\iffalse
+\DeclareOption{openbib}{\let\if@openbib\iftrue}
+
+% languages
+\let\switcht@@therlang\relax
+\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
+\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
+
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+
+\ProcessOptions
+
+\LoadClass[twoside]{article}
+\RequirePackage{multicol} % needed for the list of participants, index
+
+\setlength{\textwidth}{12.2cm}
+\setlength{\textheight}{19.3cm}
+\renewcommand\@pnumwidth{2em}
+\renewcommand\@tocrmarg{3.5em}
+%
+\def\@dottedtocline#1#2#3#4#5{%
+  \ifnum #1>\c@tocdepth \else
+    \vskip \z@ \@plus.2\p@
+    {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
+               \parfillskip -\rightskip \pretolerance=10000
+     \parindent #2\relax\@afterindenttrue
+     \interlinepenalty\@M
+     \leavevmode
+     \@tempdima #3\relax
+     \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
+     {#4}\nobreak
+     \leaders\hbox{$\m@th
+        \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
+        mu$}\hfill
+     \nobreak
+     \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
+     \par}%
+  \fi}
+%
+\def\switcht@albion{%
+\def\abstractname{Abstract.}
+\def\ackname{Acknowledgement.}
+\def\andname{and}
+\def\lastandname{\unskip, and}
+\def\appendixname{Appendix}
+\def\chaptername{Chapter}
+\def\claimname{Claim}
+\def\conjecturename{Conjecture}
+\def\contentsname{Table of Contents}
+\def\corollaryname{Corollary}
+\def\definitionname{Definition}
+\def\examplename{Example}
+\def\exercisename{Exercise}
+\def\figurename{Fig.}
+\def\keywordname{{\bf Key words:}}
+\def\indexname{Index}
+\def\lemmaname{Lemma}
+\def\contriblistname{List of Contributors}
+\def\listfigurename{List of Figures}
+\def\listtablename{List of Tables}
+\def\mailname{{\it Correspondence to\/}:}
+\def\noteaddname{Note added in proof}
+\def\notename{Note}
+\def\partname{Part}
+\def\problemname{Problem}
+\def\proofname{Proof}
+\def\propertyname{Property}
+\def\propositionname{Proposition}
+\def\questionname{Question}
+\def\remarkname{Remark}
+\def\seename{see}
+\def\solutionname{Solution}
+\def\subclassname{{\it Subject Classifications\/}:}
+\def\tablename{Table}
+\def\theoremname{Theorem}}
+\switcht@albion
+% Names of theorem like environments are already defined
+% but must be translated if another language is chosen
+%
+% French section
+\def\switcht@francais{%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e.}%
+ \def\ackname{Remerciements.}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bf Mots-cl\'e:}}
+ \def\indexname{Index}
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\remarkname{Remarque}%
+ \def\seename{voir}
+ \def\solutionname{Solution}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung.}%
+ \def\ackname{Danksagung.}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}
+ \def\indexname{Index}
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}
+ \def\solutionname{L\"osung}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+
+% Ragged bottom for the actual page
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+
+\renewcommand\small{%
+   \@setfontsize\small\@ixpt{11}%
+   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+   \abovedisplayshortskip \z@ \@plus2\p@
+   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+   \def\@listi{\leftmargin\leftmargini
+               \parsep 0\p@ \@plus1\p@ \@minus\p@
+               \topsep 8\p@ \@plus2\p@ \@minus4\p@
+               \itemsep0\p@}%
+   \belowdisplayskip \abovedisplayskip
+}
+
+\frenchspacing
+\widowpenalty=10000
+\clubpenalty=10000
+
+\setlength\oddsidemargin   {63\p@}
+\setlength\evensidemargin  {63\p@}
+\setlength\marginparwidth  {90\p@}
+
+\setlength\headsep   {16\p@}
+
+\setlength\footnotesep{7.7\p@}
+\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep   {8mm\@plus 2\p@ \@minus 2\p@}
+
+\setcounter{secnumdepth}{2}
+
+\newcounter {chapter}
+\renewcommand\thechapter      {\@arabic\c@chapter}
+
+\newif\if@mainmatter \@mainmattertrue
+\newcommand\frontmatter{\cleardoublepage
+            \@mainmatterfalse\pagenumbering{Roman}}
+\newcommand\mainmatter{\cleardoublepage
+       \@mainmattertrue\pagenumbering{arabic}}
+\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
+      \@mainmatterfalse}
+
+\renewcommand\part{\cleardoublepage
+                 \thispagestyle{empty}%
+                 \if@twocolumn
+                     \onecolumn
+                     \@tempswatrue
+                   \else
+                     \@tempswafalse
+                 \fi
+                 \null\vfil
+                 \secdef\@part\@spart}
+
+\def\@part[#1]#2{%
+    \ifnum \c@secnumdepth >-2\relax
+      \refstepcounter{part}%
+      \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
+    \else
+      \addcontentsline{toc}{part}{#1}%
+    \fi
+    \markboth{}{}%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \ifnum \c@secnumdepth >-2\relax
+       \huge\bfseries \partname~\thepart
+       \par
+       \vskip 20\p@
+     \fi
+     \Huge \bfseries #2\par}%
+    \@endpart}
+\def\@spart#1{%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \Huge \bfseries #1\par}%
+    \@endpart}
+\def\@endpart{\vfil\newpage
+              \if@twoside
+                \null
+                \thispagestyle{empty}%
+                \newpage
+              \fi
+              \if@tempswa
+                \twocolumn
+              \fi}
+
+\newcommand\chapter{\clearpage
+                    \thispagestyle{empty}%
+                    \global\@topnum\z@
+                    \@afterindentfalse
+                    \secdef\@chapter\@schapter}
+\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
+                       \if@mainmatter
+                         \refstepcounter{chapter}%
+                         \typeout{\@chapapp\space\thechapter.}%
+                         \addcontentsline{toc}{chapter}%
+                                  {\protect\numberline{\thechapter}#1}%
+                       \else
+                         \addcontentsline{toc}{chapter}{#1}%
+                       \fi
+                    \else
+                      \addcontentsline{toc}{chapter}{#1}%
+                    \fi
+                    \chaptermark{#1}%
+                    \addtocontents{lof}{\protect\addvspace{10\p@}}%
+                    \addtocontents{lot}{\protect\addvspace{10\p@}}%
+                    \if@twocolumn
+                      \@topnewpage[\@makechapterhead{#2}]%
+                    \else
+                      \@makechapterhead{#2}%
+                      \@afterheading
+                    \fi}
+\def\@makechapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \ifnum \c@secnumdepth >\m@ne
+      \if@mainmatter
+        \large\bfseries \@chapapp{} \thechapter
+        \par\nobreak
+        \vskip 20\p@
+      \fi
+    \fi
+    \interlinepenalty\@M
+    \Large \bfseries #1\par\nobreak
+    \vskip 40\p@
+  }}
+\def\@schapter#1{\if@twocolumn
+                   \@topnewpage[\@makeschapterhead{#1}]%
+                 \else
+                   \@makeschapterhead{#1}%
+                   \@afterheading
+                 \fi}
+\def\@makeschapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \normalfont
+    \interlinepenalty\@M
+    \Large \bfseries  #1\par\nobreak
+    \vskip 40\p@
+  }}
+
+\renewcommand\section{\@startsection{section}{1}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {12\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\large\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {8\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\normalsize\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\bfseries\boldmath}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+                       {-12\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\itshape}}
+\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
+                  \string\subparagraph\space with this class}\vskip0.5cm
+You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
+
+\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
+\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
+\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
+\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
+\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
+\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
+\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
+\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
+\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
+\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
+\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
+
+\let\footnotesize\small
+
+\if@custvec
+\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
+{\mbox{\boldmath$\textstyle#1$}}
+{\mbox{\boldmath$\scriptstyle#1$}}
+{\mbox{\boldmath$\scriptscriptstyle#1$}}}
+\fi
+
+\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
+\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
+\penalty50\hskip1em\null\nobreak\hfil\squareforqed
+\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
+
+\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+\gets\cr\to\cr}}}}}
+\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+<\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
+>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.8pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
+\def\bbbr{{\rm I\!R}} %reelle Zahlen
+\def\bbbm{{\rm I\!M}}
+\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
+\def\bbbf{{\rm I\!F}}
+\def\bbbh{{\rm I\!H}}
+\def\bbbk{{\rm I\!K}}
+\def\bbbp{{\rm I\!P}}
+\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
+{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
+\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
+\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbs{{\mathchoice
+{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
+\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
+{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
+
+\let\ts\,
+
+\setlength\leftmargini  {17\p@}
+\setlength\leftmargin    {\leftmargini}
+\setlength\leftmarginii  {\leftmargini}
+\setlength\leftmarginiii {\leftmargini}
+\setlength\leftmarginiv  {\leftmargini}
+\setlength  \labelsep  {.5em}
+\setlength  \labelwidth{\leftmargini}
+\addtolength\labelwidth{-\labelsep}
+
+\def\@listI{\leftmargin\leftmargini
+            \parsep 0\p@ \@plus1\p@ \@minus\p@
+            \topsep 8\p@ \@plus2\p@ \@minus4\p@
+            \itemsep0\p@}
+\let\@listi\@listI
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+              \labelwidth\leftmarginii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus2\p@ \@minus\p@}
+\def\@listiii{\leftmargin\leftmarginiii
+              \labelwidth\leftmarginiii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus\p@\@minus\p@
+              \parsep    \z@
+              \partopsep \p@ \@plus\z@ \@minus\p@}
+
+\renewcommand\labelitemi{\normalfont\bfseries --}
+\renewcommand\labelitemii{$\m@th\bullet$}
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
+                                                    {{\contentsname}}}
+ \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
+ \def\lastand{\ifnum\value{auco}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{auco}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \@starttoc{toc}\if@restonecol\twocolumn\fi}
+
+\def\l@part#1#2{\addpenalty{\@secpenalty}%
+   \addvspace{2em plus\p@}%  % space above part line
+   \begingroup
+     \parindent \z@
+     \rightskip \z@ plus 5em
+     \hrule\vskip5pt
+     \large               % same size as for a contribution heading
+     \bfseries\boldmath   % set line in boldface
+     \leavevmode          % TeX command to enter horizontal mode.
+     #1\par
+     \vskip5pt
+     \hrule
+     \vskip1pt
+     \nobreak             % Never break after part entry
+   \endgroup}
+
+\def\@dotsep{2}
+
+\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
+{chapter.\thechapter}\fi}
+
+\def\addnumcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
+                     {\thechapter}#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmarkwop#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}
+
+\def\@adcmk[#1]{\ifcase #1 \or
+\def\@gtempa{\addnumcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmarkwop}%
+  \fi\@gtempa{toc}{chapter}}
+\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
+
+\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
+ \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
+ \else
+      \nobreak
+      \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+      \@dotsep mu$}\hfill
+      \nobreak\hbox to\@pnumwidth{\hss #2}%
+ \fi\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@title#1#2{\addpenalty{-\@highpenalty}
+ \addvspace{8pt plus 1pt}
+ \@tempdima \z@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ #1\nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@author#1#2{\addpenalty{\@highpenalty}
+ \@tempdima=\z@ %15\p@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
+ \textit{#1}\par
+ \penalty\@highpenalty \endgroup}
+
+\setcounter{tocdepth}{0}
+\newdimen\tocchpnum
+\newdimen\tocsecnum
+\newdimen\tocsectotal
+\newdimen\tocsubsecnum
+\newdimen\tocsubsectotal
+\newdimen\tocsubsubsecnum
+\newdimen\tocsubsubsectotal
+\newdimen\tocparanum
+\newdimen\tocparatotal
+\newdimen\tocsubparanum
+\tocchpnum=\z@            % no chapter numbers
+\tocsecnum=15\p@          % section 88. plus 2.222pt
+\tocsubsecnum=23\p@       % subsection 88.8 plus 2.222pt
+\tocsubsubsecnum=27\p@    % subsubsection 88.8.8 plus 1.444pt
+\tocparanum=35\p@         % paragraph 88.8.8.8 plus 1.666pt
+\tocsubparanum=43\p@      % subparagraph 88.8.8.8.8 plus 1.888pt
+\def\calctocindent{%
+\tocsectotal=\tocchpnum
+\advance\tocsectotal by\tocsecnum
+\tocsubsectotal=\tocsectotal
+\advance\tocsubsectotal by\tocsubsecnum
+\tocsubsubsectotal=\tocsubsectotal
+\advance\tocsubsubsectotal by\tocsubsubsecnum
+\tocparatotal=\tocsubsubsectotal
+\advance\tocparatotal by\tocparanum}
+\calctocindent
+
+\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
+\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
+\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
+\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
+\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
+
+\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
+ \@starttoc{lof}\if@restonecol\twocolumn\fi}
+\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
+
+\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
+ \@starttoc{lot}\if@restonecol\twocolumn\fi}
+\let\l@table\l@figure
+
+\renewcommand\listoffigures{%
+    \section*{\listfigurename
+      \@mkboth{\listfigurename}{\listfigurename}}%
+    \@starttoc{lof}%
+    }
+
+\renewcommand\listoftables{%
+    \section*{\listtablename
+      \@mkboth{\listtablename}{\listtablename}}%
+    \@starttoc{lot}%
+    }
+
+\ifx\oribibl\undefined
+\ifx\citeauthoryear\undefined
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \def\@biblabel##1{##1.}
+      \small
+      \list{\@biblabel{\@arabic\c@enumiv}}%
+           {\settowidth\labelwidth{\@biblabel{#1}}%
+            \leftmargin\labelwidth
+            \advance\leftmargin\labelsep
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
+     {\let\protect\noexpand\immediate
+     \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\newcount\@tempcntc
+\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
+  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
+    {\@ifundefined
+       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
+        ?}\@warning
+       {Citation `\@citeb' on page \thepage \space undefined}}%
+    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
+     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
+       \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
+     \else
+      \advance\@tempcntb\@ne
+      \ifnum\@tempcntb=\@tempcntc
+      \else\advance\@tempcntb\m@ne\@citeo
+      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
+\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
+               \@citea\def\@citea{,\,\hskip\z@skip}%
+               \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
+               {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
+                \def\@citea{--}\fi
+      \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
+\else
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \small
+      \list{}%
+           {\settowidth\labelwidth{}%
+            \leftmargin\parindent
+            \itemindent=-\parindent
+            \labelsep=\z@
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+      \def\@cite#1{#1}%
+      \def\@lbibitem[#1]#2{\item[]\if@filesw
+        {\def\protect##1{\string ##1\space}\immediate
+      \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+   \fi
+\else
+\@cons\@openbib@code{\noexpand\small}
+\fi
+
+\def\idxquad{\hskip 10\p@}% space that divides entry from number
+
+\def\@idxitem{\par\hangindent 10\p@}
+
+\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
+                \noindent\hangindent\wd0\box0}% index entry
+
+\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
+                \noindent\hangindent\wd0\box0}% order index entry
+
+\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
+
+\renewenvironment{theindex}
+               {\@mkboth{\indexname}{\indexname}%
+                \thispagestyle{empty}\parindent\z@
+                \parskip\z@ \@plus .3\p@\relax
+                \let\item\par
+                \def\,{\relax\ifmmode\mskip\thinmuskip
+                             \else\hskip0.2em\ignorespaces\fi}%
+                \normalfont\small
+                \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
+                }
+                {\end{multicols}}
+
+\renewcommand\footnoterule{%
+  \kern-3\p@
+  \hrule\@width 2truecm
+  \kern2.6\p@}
+  \newdimen\fnindent
+  \fnindent1em
+\long\def\@makefntext#1{%
+    \parindent \fnindent%
+    \leftskip \fnindent%
+    \noindent
+    \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
+
+\long\def\@makecaption#1#2{%
+  \vskip\abovecaptionskip
+  \sbox\@tempboxa{{\bfseries #1.} #2}%
+  \ifdim \wd\@tempboxa >\hsize
+    {\bfseries #1.} #2\par
+  \else
+    \global \@minipagefalse
+    \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
+  \fi
+  \vskip\belowcaptionskip}
+
+\def\fps@figure{htbp}
+\def\fnum@figure{\figurename\thinspace\thefigure}
+\def \@floatboxreset {%
+        \reset@font
+        \small
+        \@setnobreak
+        \@setminipage
+}
+\def\fps@table{htbp}
+\def\fnum@table{\tablename~\thetable}
+\renewenvironment{table}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@float{table}}
+               {\end@float}
+\renewenvironment{table*}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@dblfloat{table}}
+               {\end@dblfloat}
+
+\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
+  ext@#1\endcsname}{#1}{\protect\numberline{\csname
+  the#1\endcsname}{\ignorespaces #2}}\begingroup
+    \@parboxrestore
+    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+  \endgroup}
+
+% LaTeX does not provide a command to enter the authors institute
+% addresses. The \institute command is defined here.
+
+\newcounter{@inst}
+\newcounter{@auth}
+\newcounter{auco}
+\newdimen\instindent
+\newbox\authrun
+\newtoks\authorrunning
+\newtoks\tocauthor
+\newbox\titrun
+\newtoks\titlerunning
+\newtoks\toctitle
+
+\def\clearheadinfo{\gdef\@author{No Author Given}%
+                   \gdef\@title{No Title Given}%
+                   \gdef\@subtitle{}%
+                   \gdef\@institute{No Institute Given}%
+                   \gdef\@thanks{}%
+                   \global\titlerunning={}\global\authorrunning={}%
+                   \global\toctitle={}\global\tocauthor={}}
+
+\def\institute#1{\gdef\@institute{#1}}
+
+\def\institutename{\par
+ \begingroup
+ \parskip=\z@
+ \parindent=\z@
+ \setcounter{@inst}{1}%
+ \def\and{\par\stepcounter{@inst}%
+ \noindent$^{\the@inst}$\enspace\ignorespaces}%
+ \setbox0=\vbox{\def\thanks##1{}\@institute}%
+ \ifnum\c@@inst=1\relax
+   \gdef\fnnstart{0}%
+ \else
+   \xdef\fnnstart{\c@@inst}%
+   \setcounter{@inst}{1}%
+   \noindent$^{\the@inst}$\enspace
+ \fi
+ \ignorespaces
+ \@institute\par
+ \endgroup}
+
+\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
+   {\star\star\star}\or \dagger\or \ddagger\or
+   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
+   \or \ddagger\ddagger \else\@ctrerr\fi}}
+
+\def\inst#1{\unskip$^{#1}$}
+\def\fnmsep{\unskip$^,$}
+\def\email#1{{\tt#1}}
+\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
+\@ifpackageloaded{babel}{%
+\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
+\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
+\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+}{\switcht@@therlang}%
+}
+\def\homedir{\~{ }}
+
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\clearheadinfo
+
+\renewcommand\maketitle{\newpage
+  \refstepcounter{chapter}%
+  \stepcounter{section}%
+  \setcounter{section}{0}%
+  \setcounter{subsection}{0}%
+  \setcounter{figure}{0}
+  \setcounter{table}{0}
+  \setcounter{equation}{0}
+  \setcounter{footnote}{0}%
+  \begingroup
+    \parindent=\z@
+    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+    \if@twocolumn
+      \ifnum \col@number=\@ne
+        \@maketitle
+      \else
+        \twocolumn[\@maketitle]%
+      \fi
+    \else
+      \newpage
+      \global\@topnum\z@   % Prevents figures from going at top of page.
+      \@maketitle
+    \fi
+    \thispagestyle{empty}\@thanks
+%
+    \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
+    \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
+    \instindent=\hsize
+    \advance\instindent by-\headlineindent
+    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
+       \addcontentsline{toc}{title}{\the\toctitle}\fi
+    \if@runhead
+       \if!\the\titlerunning!\else
+         \edef\@title{\the\titlerunning}%
+       \fi
+       \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
+       \ifdim\wd\titrun>\instindent
+          \typeout{Title too long for running head. Please supply}%
+          \typeout{a shorter form with \string\titlerunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\titrun=\hbox{\small\rm
+          Title Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@title{\copy\titrun}%
+    \fi
+%
+    \if!\the\tocauthor!\relax
+      {\def\and{\noexpand\protect\noexpand\and}%
+      \protected@xdef\toc@uthor{\@author}}%
+    \else
+      \def\\{\noexpand\protect\noexpand\newline}%
+      \protected@xdef\scratch{\the\tocauthor}%
+      \protected@xdef\toc@uthor{\scratch}%
+    \fi
+    \addcontentsline{toc}{author}{\toc@uthor}%
+    \if@runhead
+       \if!\the\authorrunning!
+         \value{@inst}=\value{@auth}%
+         \setcounter{@auth}{1}%
+       \else
+         \edef\@author{\the\authorrunning}%
+       \fi
+       \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}%
+       \ifdim\wd\authrun>\instindent
+          \typeout{Names of authors too long for running head. Please supply}%
+          \typeout{a shorter form with \string\authorrunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\authrun=\hbox{\small\rm
+          Authors Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@author{\copy\authrun}%
+       \markboth{\@author}{\@title}%
+     \fi
+  \endgroup
+  \setcounter{footnote}{\fnnstart}%
+  \clearheadinfo}
+%
+\def\@maketitle{\newpage
+ \markboth{}{}%
+ \def\lastand{\ifnum\value{@inst}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{@inst}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \begin{center}%
+ \let\newline\\
+ {\Large \bfseries\boldmath
+  \pretolerance=10000
+  \@title \par}\vskip .8cm
+\if!\@subtitle!\else {\large \bfseries\boldmath
+  \vskip -.65cm
+  \pretolerance=10000
+  \@subtitle \par}\vskip .8cm\fi
+ \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
+ \def\thanks##1{}\@author}%
+ \global\value{@inst}=\value{@auth}%
+ \global\value{auco}=\value{@auth}%
+ \setcounter{@auth}{1}%
+{\lineskip .5em
+\noindent\ignorespaces
+\@author\vskip.35cm}
+ {\small\institutename}
+ \end{center}%
+ }
+
+% definition of the "\spnewtheorem" command.
+%
+% Usage:
+%
+%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
+% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
+% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
+%
+% New is "cap_font" and "body_font". It stands for
+% fontdefinition of the caption and the text itself.
+%
+% "\spnewtheorem*" gives a theorem without number.
+%
+% A defined spnewthoerem environment is used as described
+% by Lamport.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@thmcountersep{}
+\def\@thmcounterend{.}
+
+\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
+
+% definition of \spnewtheorem with number
+
+\def\@spnthm#1#2{%
+  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
+\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
+
+\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}\@addtoreset{#1}{#3}%
+   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
+     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+                              \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}%
+   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
+                               \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spothm#1[#2]#3#4#5{%
+  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
+  {\expandafter\@ifdefinable\csname #1\endcsname
+  {\global\@namedef{the#1}{\@nameuse{the#2}}%
+  \expandafter\xdef\csname #1name\endcsname{#3}%
+  \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
+  \global\@namedef{end#1}{\@endtheorem}}}}
+
+\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\refstepcounter{#1}%
+\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
+
+\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
+                    \ignorespaces}
+
+\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
+       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
+
+\def\@spbegintheorem#1#2#3#4{\trivlist
+                 \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
+
+\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
+      \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
+
+% definition of \spnewtheorem* without number
+
+\def\@sthm#1#2{\@Ynthm{#1}{#2}}
+
+\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
+    \expandafter\xdef\csname #1name\endcsname{#2}%
+    \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
+
+\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
+
+\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
+       {#4}{#2}{#3}\ignorespaces}
+
+\def\@Begintheorem#1#2#3{#3\trivlist
+                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
+
+\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
+      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
+
+\if@envcntsect
+   \def\@thmcountersep{.}
+   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
+\else
+   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
+   \if@envcntreset
+      \@addtoreset{theorem}{section}
+   \else
+      \@addtoreset{theorem}{chapter}
+   \fi
+\fi
+
+%definition of divers theorem environments
+\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
+\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
+\if@envcntsame % alle Umgebungen wie Theorem.
+   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
+\else % alle Umgebungen mit eigenem Zaehler
+   \if@envcntsect % mit section numeriert
+      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
+   \else % nicht mit section numeriert
+      \if@envcntreset
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{section}}
+      \else
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{chapter}}%
+      \fi
+   \fi
+\fi
+\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
+\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
+\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
+\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
+\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
+\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
+\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
+\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
+\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
+\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
+\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
+\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
+\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
+\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
+
+\def\@takefromreset#1#2{%
+    \def\@tempa{#1}%
+    \let\@tempd\@elt
+    \def\@elt##1{%
+        \def\@tempb{##1}%
+        \ifx\@tempa\@tempb\else
+            \@addtoreset{##1}{#2}%
+        \fi}%
+    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
+    \expandafter\def\csname cl@#2\endcsname{}%
+    \@tempc
+    \let\@elt\@tempd}
+
+\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+      \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
+                  \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+      \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
+      }
+
+\renewenvironment{abstract}{%
+      \list{}{\advance\topsep by0.35cm\relax\small
+      \leftmargin=1cm
+      \labelwidth=\z@
+      \listparindent=\z@
+      \itemindent\listparindent
+      \rightmargin\leftmargin}\item[\hskip\labelsep
+                                    \bfseries\abstractname]}
+    {\endlist}
+
+\newdimen\headlineindent             % dimension for space between
+\headlineindent=1.166cm              % number and text of headings.
+
+\def\ps@headings{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \leftmark\hfil}
+   \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \hfil}
+   \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\if@runhead\ps@headings\else
+\ps@empty\fi
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\endinput
+%end of file llncs.cls
diff --git a/helm/mathql/doc/mathql.tex b/helm/mathql/doc/mathql.tex
index 1dde6905f..ed9a96021 100644
--- a/helm/mathql/doc/mathql.tex
+++ b/helm/mathql/doc/mathql.tex
@@ -1,27 +1,32 @@
-\documentclass[10pt]{article}
+\documentclass{llncs}
 
 \usepackage{mathql_macros}
 
-\addtolength{\textheight}{2.5cm}
-\addtolength{\oddsidemargin}{-1.0cm}
-\addtolength{\evensidemargin}{-1.0cm}
-\addtolength{\textwidth}{2.0cm}
-\addtolength{\topmargin}{-1.0cm}
-
 \title{MathQL-1 Version 4\\Reference Documentation}
-\author{Ferruccio Guidi}
+\author{Ferruccio Guidi%
+\thanks{This work has been partially supported by
+MoWGLI (European FET Project IST-2001-33562).}
+}
+
+\institute{Department of Computer Science\\
+Mura Anteo Zamboni 7, 40127 Bologna, ITALY.\\
+\email{fguidi@cs.unibo.it}}
 
-\bibliographystyle{numeric}
+\date{ }
 
 \begin{document}
 
 \maketitle
 
+\begin{abstract}
+\end{abstract}
+
 \tableofcontents
 
 \input{mathql_overview}
 \input{mathql_introduction}
 \input{mathql_operational}
+\input{mathql_tests}
 \input{mathql_bib}
 
 \end{document}
diff --git a/helm/mathql/doc/mathql_bib.tex b/helm/mathql/doc/mathql_bib.tex
index 32b71ed40..be28be8ff 100644
--- a/helm/mathql/doc/mathql_bib.tex
+++ b/helm/mathql/doc/mathql_bib.tex
@@ -38,7 +38,6 @@ FrancoAngeli, 1998.
 D. Lordi:
 \emph{Sperimentazione e Sviluppo di Strumenti per la gestione di metadati}. \\
 Master Thesis in Computer Science, University of Bologna, 2002.
-Advisor: A. Asperti.
 
 \bibitem {RDF}
 \emph{Resource Description Framework (RDF) Model and Syntax Specification}.
diff --git a/helm/mathql/doc/mathql_introduction.tex b/helm/mathql/doc/mathql_introduction.tex
index 61cc88c02..0fad196e0 100644
--- a/helm/mathql/doc/mathql_introduction.tex
+++ b/helm/mathql/doc/mathql_introduction.tex
@@ -1,15 +1,15 @@
-\section{Introduction}
+\section{The language}
 
 This paper presents {\MathQL} version 4 which is the latest version of the
-language, fully developed by Ferruccio Guidi.  
+language, fully developed by the Author.
 For a description of the previous versions of {\MathQL} see: \cite{Gui03}
 (version 3), \cite{GS03} (version 2), \cite{Lor02} (version 1).
 The main novelties of this version are the elimination of some cast operators
-(producing a substantial simplification in the query structure and semantics,
-see \secref{Operational}), a clear distinction between the core language and
-the auxiliary functions of the basic library, a support for query generating
-functions, the possibility of extending the language adding new libraries of
-functions and a more uniform textual syntax. 
+(producing a substantial simplification in the query structure and semantics),
+a clear distinction between the core language and the auxiliary functions of
+the basic library, a support for query generating functions, the possibility
+of extending the language adding new libraries of functions and a more uniform
+textual syntax. 
 {\MathQL}.4 incorporates the features of {\MathQL}.3 not documented on paper%
 \footnote
 {See the ``what's new'' section of {\MathQL} Web Site:
@@ -21,4 +21,4 @@ the query results.
 \input{mathql_introduction_property}
 \input{mathql_introduction_core}
 \input{mathql_introduction_basic}
-% \input{mathql_introduction_textual}
+\input{mathql_introduction_textual}
diff --git a/helm/mathql/doc/mathql_introduction_avsets.tex b/helm/mathql/doc/mathql_introduction_avsets.tex
index d9943f1cf..20e826403 100644
--- a/helm/mathql/doc/mathql_introduction_avsets.tex
+++ b/helm/mathql/doc/mathql_introduction_avsets.tex
@@ -1,4 +1,4 @@
-\subsection {Sets of attributed values.}
+\subsection {Sets of attributed values.} \label{AVSets}
 
 The data representation model used by {\MathQL} relies on the notion of 
 \emph{set of attributed values} ({\av} set for short) that is, in practice,
@@ -10,7 +10,7 @@ should be driven from the {\RDFS} class system. This may be a future
 improvement.}
 Each {\av} in an {\av} set consists of a string% 
 \footnote{When we say \emph{string}, we mean a finite sequence of characters.}
-(that we call the \emph{head string} or \emph{value}) and a (possibly emty)
+(that we call the \emph{head string} or \emph{value}) and a (possibly empty)
 multiset of named attributes whose content is a set of strings.
 Attribute names are made of a (possibly empty) list of string components, so
 they can be hierarchically structured. 
@@ -18,7 +18,7 @@ Moreover the attributes of a value are partitioned into a set of \emph{groups}
 ({\ie} subsets) to improve its structure.
 
 In the above description a \emph{set} is an \emph{unordered} finite
-sequence \emph{without} repetitions wheras a \emph{multiset} is an
+sequence \emph{without} repetitions whereas a \emph{multiset} is an
 \emph{unordered} finite sequence \emph{with} repetitions.
 
 In the present context repetitions are defined as follows:
@@ -33,7 +33,7 @@ definition of an {\av} set is just the right one among the many alternatives
 that were tried.} 
 
 As we said, {\MathQL}.4 uses {\av} sets to represent many kinds of
-information, namely:
+information:
 
 \begin{enumerate}
 
@@ -50,26 +50,25 @@ objects of repeated predicates.
 Moreover structured attribute names can encode various components of
 structured properties preserving their semantics.
 
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 The RDF triples:
-("http://www.w3.org/2002/01/rdf-databases/protocol", "dc:creator", "Sandro Hawke")
-("http://www.w3.org/2002/01/rdf-databases/protocol", "dc:creator", "Eric Prud'hommeaux")
-("http://www.w3.org/2002/01/rdf-databases/protocol", "dc:date", "2002-01-08")
+ ("protocol", "dc:creator", "Sandro Hawke")
+ ("protocol", "dc:creator", "Eric Prud'hommeaux")
+ ("protocol", "dc:date", "2002-01-08")
 
 The corresponding attributed value:
-"http://www.w3.org/2002/01/rdf-databases/protocol" attr
-             {"dc:creator" = {"Sandro Hawke", "Eric Prud'hommeaux"}; "dc:date" = "2002-01-08"}
+ "protocol" attr {/"dc:creator" = {"Sandro Hawke", "Eric Prud'hommeaux"};
+                  /"dc:date" = "2002-01-08"}
 \end{verbatim} \end{footnotesize}
-\vskip-1pc
+\vspace{-1pc}
 \caption{The representation of a pool of {\RDF} triples} \label{AVOne}
 \end{figure}
 
 \figref{AVOne} shows how a set of triples can be coded in an {\av}.
-Note that the word \emph{attr} separates the head string from its attributes,
+Note that the word \TT{attr} separates the head string from its attributes,
 braces enclose an attribute group in which attributes are separated by
-semicolons, and an equal sign separates an attribute name from its contents
-(see \subsecref{Textual} for the complete {\av} syntax).
+semicolons, and an equal sign separates an attribute name from its contents.
 
 In this setting the grouping feature can be used to separate semantically
 different classes of properties associated to a resource (as for instance
@@ -77,7 +76,7 @@ Dublin Core metadata, Euler metadata and user-defined metadata).
 
 \item
 A pool of arbitrarily chosen {\RDF} triples is encoded in an {\av} set 
-placing different {\av}'s the subset of triples sharing the same subject.
+placing in each {\av} the subset of triples sharing the same head string.
 
 Note that the use of {\av} sets to build query results allows {\MathQL} queries
 to return sets of {\RDF} triples instead of mere sets of resources, in the
@@ -90,22 +89,19 @@ which holds the head strings).
 \figref{Table} shows an {\av} set describing the properties of two resources
 ``A'' and ``B'' giving its table representation, in which the columns
 corresponding to attributes in the same group are clustered between
-double-line delimiters%
+double-line delimiters.%
 \footnote{A table with grouped labelled columns like the one above resembles a
-set of relational database tables.}.   
+set of relational database tables.}   
 
-%Another possible use of a {\MathQL} query result is for the encoding of a
-%relational database table: in this sense the indexed column is stored in the
-%subject strings, the names of the other columns are stored in attribute names
-%and cell contents are stored in attribute values.
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
-"A" attr {"major" = "1"; "minor" = "2"}, {"first" = "2002-01-01"; "modified" = "2002-03-01"};
-"B" attr {"major" = "1"; "minor" = "7"}, {"first" = "2002-02-01"; "modified" = "2002-04-01"}
+"A" attr {/"major" = "1"; /"minor" = "2"}, 
+         {/"first" = "2002-01-01"; /"modified" = "2002-03-01"};
+"B" attr {/"major" = "1"; /"minor" = "7"}, 
+         {/"first" = "2002-02-01"; /"modified" = "2002-04-01"}
 \end{verbatim}
 \begin{center} \begin{tabular}{|c||c|c||c|c||}
-\hline   & {\bf ``major''} & {\bf ``minor''} & {\bf ``first''} & {\bf ``modified''} \\
+\hline   & \textbf{``major''} & \textbf{``minor''} & \textbf{``first''} & \textbf{``modified''} \\
 \hline ``A'' & ``1'' & ``2'' & ``2002-01-01'' & ``2002-03-01'' \\
 \hline ``B'' & ``1'' & ``7'' & ``2002-02-01'' & ``2002-04-01'' \\
 \hline
@@ -118,15 +114,14 @@ a query result) which fits in 4 dimensions: namely we can extend independently
 the set of the head strings (dimension 1), the attributes in each group
 (dimension 2), the groups in each {\av} (dimension 3) and the contents of each
 attribute (dimension 4).
-
 The metadata defined in the table of \figref{Table} will be used in subsequent
 examples.
-For this purpose assume that \TT{first} and \TT{modified} are the components
-of a structured property \TT{date} available for the resources ``A'' and ``B''.
+For this purpose assume that ``first'' and ``modified'' are the components
+of a structured property ``date'' available for the resources ``A'' and ``B''.
 
 \item
-The value of an {\RDF} property is encoded in a single {\av} distinguishing
-three situations:
+The value of an {\RDF} property is encoded in an {\av} distinguishing three
+cases:
 
 \begin{itemize}
 
@@ -142,49 +137,49 @@ the content of this component is placed in the {\av} head string and the
 other components are stored in the {\av} attributes as in the case 1.
 
 \item
-If the property is structured and its value does not have a main component,
-the {\av} head string is empty and the components are stored in the
-attributes.
+For the value of a structured property without a main component, the head
+string is empty and the components are stored in the attributes.
 
 \end{itemize}
 
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 First example, one instance:
-"" attr {"major" = "1"; "minor" = "2"};  no main component
-"1" attr {"minor" = "2"};                main component is "major"
-"2" attr {"major" = "1"}                 main component is "minor"
+ "" attr {/"major" = "1"; /"minor" = "2"} no main component
+ "1" attr {/"minor" = "2"} main component is "major"
+ "2" attr {/"major" = "1"} main component is "minor"
 
 Second example: two separate instances:
-"" attr {"major" = "1"; "minor" = "2"}, {"major" = "1"; "minor" = "7"}; no main component
-"1" attr {"minor" = "2"}, {"minor" = "7"}                            main component is "major"
+ "" attr {/"major" = "1"; /"minor" = "2"}, 
+         {/"major" = "1"; /"minor" = "7"} no main component
+ "1" attr {/"minor" = "2"}, {/"minor" = "7"} main component is "major"
 
 Third example: two mixed instances:
-"" attr {"major" = "3", "6"; "minor" = "4", "9"} no main component
+ "" attr {/"major" = "3", "6"; /"minor" = {"4", "9"}} no main component
 \end{verbatim} \end{footnotesize}
-\vskip-1pc
+\vspace{-1pc}
 \caption{The representation of the structured value of a property}
 \label{AVTwo}
 \end{figure}
 
 \figref{AVTwo} (first example) shows three possible ways of representing in
-{\av}'s an instance of a structured property \TT{id} whose value has two
-fields ({\ie} properties) \TT{major} and \TT{minor}.
-In this instance, \TT{major} is set to ``1'' and \TT{minor} is set to ``2''.
-The representations depend on which component of \TT{id} is chosen as the
-main component (none, \TT{major} or \TT{minor} respectively).
+{\av}'s an instance of a structured property ``id'' whose value has two
+fields ({\ie} properties) ``major'' and ``minor''.
+In this instance, ``major'' is set to ``1'' and ``minor'' is set to ``2''.
+The representations depend on which component of ``id'' is chosen as the
+main component (none, ``major'' or ``minor'' respectively).
 Several structured property values sharing a common main component can be
 encodes in a single {\av} exploiting the grouping facility: in this case the
 attributes of every instance are enclosed in separate groups.
 \figref{AVTwo} (second example) shows the representations of two instances of
-\TT{id}: the previous one and a new one for which \TT{major} is ``1'' and
-\TT{minor} is ``7''.
+``id'': the former and a new one for which ``major'' is ``1'' and ``minor'' is
+``7''.
 
 Note that if the attributes of the two groups are encoded in a single group,
 the notion of which components belong to the same property value can not be
 recovered in the general case because the values of an attribute form a set
-and thus are unordered. \newline
-As an example think of two instances of \TT{id} encoded as in \figref{AVTwo}
+and thus are unordered.
+As an example think of two instances of ``id'' encoded as in \figref{AVTwo}
 (third example).
 
 \item
@@ -199,7 +194,7 @@ head string and no attributes.
 
 \end{enumerate}
 
-{\MathQL} defines five binary operations on {\av} sets: two unions, two
+{\MathQL} defines five core binary operations on {\av} sets: two unions, two
 intersections and a difference. The first four are defined in terms of an
 operation, that we call \emph{addition}, involving two {\av}'s with the same
 head string.
@@ -209,47 +204,47 @@ two ways to compose the attribute groups:
 \begin{itemize}
 
 \item
-With the \emph{set-theoretic} addition, the set of attribute groups in the
+with the \emph{set-theoretic} addition, the set of attribute groups in the
 resulting {\av} is the set-theoretic union of the sets of attribute groups in
-the operands.
+the operands;
 
 \item
-With the \emph{distributive} addition, the set of attribute groups in the
+with the \emph{distributive} addition, the set of attribute groups in the
 resulting {\av} is the ``Cartesian product'' of the sets of attribute groups
 in the two operands. 
-In this context, an element of the ``Cartesian product'' is not a pair of
-groups but it is the set-theoretic union of these groups where the contents of
-homonymous attributes are clustered together using set-theoretic unions.
+Here an element of the ``Cartesian product'' is not a pair of groups but it is
+the set-theoretic union of these groups where the contents of homonymous
+attributes are clustered together using set-theoretic unions.
 
 \end{itemize}
 
 \figref{Addition} shows an example of the two kinds of addition.
 
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 Attributed values used as operands for the addition:
-"1" attr {"A" = "a"}, {"B" = "b1"}
-"1" attr {"A" = "a"}, {"B" = "b2"}
+ "1" attr {/"A" = "a"}, {/"B" = "b1"}
+ "1" attr {/"A" = "a"}, {/"B" = "b2"}
 
 Set-theoretic addition:
-"1" attr {"A" = "a"}, {"B" = "b1"}, {"B" = "b2"}
+" 1" attr {/"A" = "a"}, {/"B" = "b1"}, {/"B" = "b2"}
 
 Distributive addition:
-"1" attr {"A" = "a"}, {"A" = "a"; "B" = "b2"}, {"B" = "b1"; "A" = "a"}, {"B" = {"b1", "b2"}}
+ "1" attr {/"A" = "a"}, {/"A" = "a"; /"B" = "b2"}, 
+          {/"B" = "b1"; /"A" = "a"}, {/"B" = {"b1", "b2"}}
 \end{verbatim} \end{footnotesize}
-\vskip-1pc
+\vspace{-1pc}
 \caption{The addition of attributed values}
 \label{Addition}
 \end{figure}
 
-Now we can discuss the five operations between {\av} sets that we mentioned
-above:
+Now we can discuss the five operations between {\av} sets:
 
 \begin{itemize}
 
 \item
-The two unions ocorresponds to the set-theoretic union of their operand where
-the {\av}'s sharing the head string are are added either set-theoretically or
+The two unions corresponds to the set-theoretic union of their operand where
+the {\av}'s sharing the head string are added either set-theoretically or
 distributively as explained above (thus we have a set-theoretic union and a
 distributive union in the two cases). In this context the empty {\av} set
 plays the role of the neutral element. 
@@ -258,8 +253,8 @@ compose the attributes of the operands preserving their group structure.
 
 \item
 The two intersections are the dual of the above unions: they contain the
-{\av}'s whose head string appears in each argument where {\av}'s sharing the
-head string are added either set-theoretically or distributively as before.
+{\av}'s whose head string appears in each argument where the {\av}'s sharing
+the head string are added either set-theoretically or distributively as before.
 
 The distributive intersection has the double benefit of filtering the
 common values of the given {\av} sets, and of merging their attribute groups
@@ -274,28 +269,28 @@ argument whose head string does not appear in the second argument.
 
 \figref{Binary} shows how the above operations work in a simple example.
 
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 Sets of attributed values used as operands for the operations:
-"1" attr {"A" = "a"}; "2" attr {"B" = "b1"} 
-"2" attr {"B" = "b2"}
+ "1" attr {/"A" = "a"}; "2" attr {/"B" = "b1"} 
+ "2" attr {/"B" = "b2"}
 
 Set-theoretic union:
-"1" attr {"A" = "a"}; "2" attr {"B" = "b1"}, {"B" = "b2"}
+ "1" attr {/"A" = "a"}; "2" attr {/"B" = "b1"}, {/"B" = "b2"}
 
 Distributive union:
-"1" attr {"A" = "a"}; "2" attr {"B" = {"b1", "b2"}}
+ "1" attr {/"A" = "a"}; "2" attr {/"B" = {"b1", "b2"}}
 
 Set-theoretic intersection:
-"2" attr {"B" = "b1"}, {"B" = "b2"}
+ "2" attr {/"B" = "b1"}, {/"B" = "b2"}
 
 Distributive intersection:
-"2" attr {"B" = {"b1", "b2"}}
+ "2" attr {/"B" = {"b1", "b2"}}
 
 Difference:
-"1" attr {"A" = "a"}
+ "1" attr {/"A" = "a"}
 \end{verbatim} \end{footnotesize}
-\vskip-1pc
+\vspace{-1pc}
 \caption{The binary operations on sets of attributed values}
 \label{Binary}
 \end{figure}
diff --git a/helm/mathql/doc/mathql_introduction_basic.tex b/helm/mathql/doc/mathql_introduction_basic.tex
new file mode 100644
index 000000000..ccf13f280
--- /dev/null
+++ b/helm/mathql/doc/mathql_introduction_basic.tex
@@ -0,0 +1,136 @@
+\subsection{The basic library} \label{Basic}
+
+The present paper leaves us too little space to present a complete
+description of {\MathQL}.4 basic library, so we only give a glance to the
+features it provides.
+
+For the user convenience {\MathQL}.4 includes a syntax extension for all the
+basic library functions, in order to hide the actual function invocation.
+
+Here are some of the provided constructions:
+
+\begin{itemize}
+
+\item 
+\textbf{Aliases for commonly used constant {\av} sets.}
+\EM{empty}, \EM{false}, \EM{true}. 
+
+\item 
+\textbf{Conditional operator.} 
+\TT{if} \EM{av-set} \TT{then} \EM{av-set} \TT{else} \EM{av-set}.
+Tests the first {\av} set for inhabitance and evaluates one of the other {\av}
+sets accordingly.
+
+\item 
+\textbf{Standard \emph{select} clause.} 
+\TT{select @}\EM{variable} \TT{from} \EM{av-set-1} \TT{where} \EM{av-set-2}.
+It is:
+\TT{for @}\EM{variable} \TT{in} \EM{av-set-1} \TT{sup}
+\TT{if} \EM{av-set-2} \TT{then @}\EM{variable} \TT{else empty}.
+
+\item
+\textbf{Set refinement}. The operator
+\TT{keep} \EM{optional-flag} \EM{name-list} \TT{in} \EM{av-set}
+removes from its argument every attribute whose name is included (or is not,
+according to the \EM{flag}) in the given \EM{name-list}.
+If the \EM{flag} is not present, the \EM{name-list} specifies the attributes
+to keep, whereas if the \EM{flag} is \TT{allbut}, the \EM{name-list} specifies
+the attributes to remove.
+Removing unwanted information from an {\av} set is useful in two cases: it
+lowers the complexity of intermediate query results increasing the performance
+of subsequent operations and it cleans the final query results making them
+easier to manage for the application that submits the query.%
+\footnote
+{Interpreting {\av} sets as relational database tables, this functionality
+allows to select the columns a table is made of, as with the {\SQL} 
+\emph{select} operator.}
+
+\item
+\textbf{projections.} 
+The operator 
+\TT{proj} \EM{name} \TT{of} \EM{av-set} makes the set-theoretic union of the
+contents that the specified attribute has in each group of the given {\av} set.
+Each element of this union then becomes the head string of an {\av} without
+attributes and the set of these is returned.%
+\footnote
+{This is the content of a labelled column of the given \EM{av-set} viewed as a
+table.} 
+See \figref{Proj}.
+
+\begin{figure}
+\begin{footnotesize} \begin{verbatim}
+proj /"name" of ["1" attr {\"name" = {"a", "b"}}, {\"name" = {"b", "c"}} 
+gives "a"; "b"; "b"
+\end{verbatim} \end{footnotesize}
+\vspace{-1pc}
+\caption{A simple projection} \label{Proj}
+\end{figure}
+
+The construction \TT{keep} \EM{av-set} is also provided to remove all the
+attributes in the given \EM{av-set} ({\ie} the list of the attributes to keep
+is empty).%
+\footnote
+{This is the content of the first column of the \EM{av-set} viewed as a table.}
+
+\item
+\textbf{Core operations on {\av} sets.}
+\EM{av-set} \EM{core-operator} \EM{av-set}
+returns an {\av} set composing the two operands according to the specified
+\EM{core-operator} (see \subsecref{AVSets}) which can be \TT{union}
+(set-theoretic union), \TT{intersect} (set-theoretic intersection) or
+\TT{diff} (difference). 
+\TT{union} and \TT{intersect} are also provided in their $n$-ary form
+($ n \ge 1 $ for \TT{intersect}) and the $n$-ary union has the syntax
+extension: 
+\verb+{+ \EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+.
+
+\item 
+\textbf{Logical operations on {\av} sets.}
+\EM{and}, \EM{or}, \EM{xor}, \EM{not}.
+They are inspired by the C-style Boolean operators defined for the
+integer numbers. In particular:
+
+\TT{not} \EM{av-set}:
+returns \emph{false} if the \EM{av-set} is inhabited, or \emph{true} otherwise.
+
+\EM{av-set-1} \TT{and} \EM{av-set-2}:
+gives \EM{av-set-2} if \EM{av-set-1} is inhabited, or \emph{false} otherwise.
+
+\EM{av-set-1} \TT{or} \EM{av-set-2}:
+returns \EM{av-set-1} if it is inhabited, or \EM{av-set-2} otherwise.
+
+\EM{av-set-1} \TT{xor} \EM{av-set-2}:
+gives \emph{false} if both av-sets are inhabited or empty, or the inhabited
+\EM{av-set} otherwise.
+
+\TT{and} and \TT{or} are also available in their $n$-ary form.
+
+\item 
+\textbf{Comparisons between {\av} sets.}
+\EM{av-set} \EM{test-operator} \EM{av-set}.
+Following the repetition rules of {\av} sets presented in \subsecref{AVSets},
+these operators work just on the head strings of their arguments and
+discard the attributes. All of them return \emph{false} or \emph{true}
+according to the outcome of the respective test. 
+The \emph{test-operator} includes: \TT{sub} (set-theoretic subset relation),
+\TT{eq} (set-theoretic quality), \TT{meet} (inhabitance of the set-theoretic
+intersection), \TT{le} (numeric less-or-equal-than), \TT{lt} (numeric
+less-than).%
+\footnote{\TT{le} and \TT{lt} return \emph{false} if their operands are invalid
+numbers.}
+
+Note that the set-theoretic ``meet'' operator 
+({\ie} $ V \meet W \equiv (\lex v \in V)\ v \in W $)
+is the natural companion of the corresponding ``sub'' operator 
+({\ie} $ V \sub W \equiv (\lall v \in V)\ v \in W $) being its logical dual
+and is already being used successfully in the context of a constructive
+({\ie} intuitionistic and predicative) approach to point-free topology
+(see \cite{Sam00} for details).
+
+\item 
+\textbf{Cardinality of an {\av} set.}
+This information is retrieved by the operator \TT{count} \EM{av-set} that
+returns an {\av} set representing a natural number.
+
+\end{itemize}
+
diff --git a/helm/mathql/doc/mathql_introduction_core.tex b/helm/mathql/doc/mathql_introduction_core.tex
index c277f1852..05f9e9fd9 100644
--- a/helm/mathql/doc/mathql_introduction_core.tex
+++ b/helm/mathql/doc/mathql_introduction_core.tex
@@ -3,107 +3,96 @@
 {\MathQL}.4 consists of a core language and of a basic library. Other
 user-defined libraries can be added at will. The core language includes the
 \TT{property} operator mentioned in \subsecref{HighAccess} that queries the
-underlying {\RDF} database and the infrastructure to post-process the
+underlying {\RDF} database, and the infrastructure to post-process the
 query results. The components of this infrastructure are listed below:
 
 \begin{itemize}
 
 \item 
-Explicit sets of attributed values.
-
+\textbf{Explicit sets of attributed values.}
 An explicit {\av} set can be placed in a query in two forms: 
-as a single quoted string, like \verb+"this is a query result"+, that
-evaluates in a single {\av} with that value and no attributes, or as a full
-{\av} set in the syntax shown in the previous sections but sorrounded by
-square brackets, like \verb+["head" attr {"attribute-name" = "contents"}]+.
-\newline
-In the second form, the contents of an attribute can be the result of a query,
-like
-\verb+["head" attr {"attribute-name" = property /"metadata" of "resource"}]+.
+as a quoted string, like \verb+"this is a query result"+, that evaluates in a
+single {\av} with that value and no attributes, or as a full {\av} set in the
+syntax shown in the previous sections but surrounded by square brackets, like 
+\verb+["head" attr {/"attribute" = "contents"}]+.
 \newline
-In this case the contents of the attribute are the head strings of the query
-result, whose attributes (if any) are discarded. 
+In the second form, the contents of an attribute can be the result of a query
+and in this case the contents of the attribute are the head strings of the
+query result, whose attributes (if any) are discarded. 
+\end{itemize}
 
-\item 
-Variable assignment.
+\begin{center}
+\verb+["head" attr {/"attribute" = property /"metadata" of "resource"}]+
+\end{center}
+
+\begin{itemize}
 
+\item 
+\textbf{Variable assignment.}
 Variables for {\av} sets (preceded by a \TT{\$} sign and called
 \emph{set variables}) can be assigned using a standard \emph{let-in}
 construction and may appear wherever an {\av} set ({\ie} a query result) is
 allowed.  
-\newline
 The assignment has the form: 
 \TT{let \$}\EM{variable} \TT{=} \EM{av-set} \TT{in} \EM{av-set}
 so we can write:
 \newline
-\verb+let $var = "contents" in ["head" attr {"attribute-name" = $var}]+.
+\verb+let $var = "contents" in ["head" attr {/"attribute" = $var}]+.
 
-The scope rules of {\MathQL} variables are tipical for an imperative
-programming language and any case of assignment propagation will be indicated.
+The scope of {\MathQL} variables is typical for an imperative programming
+language and any case of assignment propagation will be indicated.
 
 \item 
-Sequential composition.
-
+\textbf{Sequential composition.}
 This construction has the form: \EM{av-set} \TT{;;} \EM{av-set} and works as
 follows: the two {\av} sets are evaluated one after the other and the first
 one is discarded but the variables assigned in the first {\av} set are
 available to the second one.  
 
 \item 
-Unbounded iteration.
-\newline
+\textbf{Unbounded iteration.}
 This construction comes in two forms:
 
-\TT{while} \EM{av-set} \TT{sup} \EM{av-set}:
-\newline
-iterates the evaluation of the second {\av} set until the first {\av set} is
-empty and returns the {\MathQL} set-theoretic union of all the evaluiations
-of the second {\av set}.
-
-\TT{while} \EM{av-set} \TT{inf} \EM{av-set}:
-\newline
-like the former but set-theoretic intersection is used instead of
+\TT{while} \EM{av-set-1} \TT{sup} \EM{av-set-2}:
+iterates the evaluation of \EM{av-set-2} until \EM{av-set-1} is empty and
+returns the {\MathQL} set-theoretic union of all the evaluations of
+\EM{av-set-2}.
+\TT{while} \EM{av-set-1} \TT{inf} \EM{av-set-2}:
+like the former but the set-theoretic intersection is used instead of the
 set-theoretic union.
 
-In order for \TT{while} to work as expected, both {\av} sets are evaluaed in
+In order for \TT{while} to work as expected, both {\av} sets are evaluated in
 a common context during the iteration ({\ie} the variables defined in both
-are alailable to both) and this context is also propagated outside the
-\TT{while} for convenience. 
+are available to both) and this context is also propagated outside the
+\TT{while}. 
 
 \item 
-Bounded iteration.
-\newline
+\textbf{Bounded iteration.}
 Also this construction comes in two forms:
 
 \TT{for @}\EM{variable} \TT{in} \EM{av-set} \TT{sup} \EM{av-set}:
-\newline
 iterates the evaluation of the second \EM{av-set} assigning the \EM{variable} 
 to each element in the first \EM{av-set} and builds the {\MathQL}
 set-theoretic union of the obtained results.
 
 \TT{for @}\EM{variable} \TT{in} \EM{av-set} \TT{inf} \EM{av-set}:
-\newline
-like the former but set-theoretic intersection is used instead of
+like the former but the set-theoretic intersection is used instead of the
 set-theoretic union.
 
 The variables for attributed values (preceded by a \TT{@} sign and called 
 \emph{element variables}) may appear wherever an {\av} set is allowed and
 and in some additional places. 
-\newline
 The element variables are kept distinct from the set variables (therefore
 \TT{\$variable} and \TT{@variable} may appear in the same query without
-abiguity).
-
+ambiguity).
 Concerning the scope rules used in these constructions, the variables
 assigned by the first {\av} set are available to the second {\av} set during
 the iteration and the variables assigned by both {\av} sets are available 
 outside the \TT{for} as in the previous case. 
 
 \item
-Addition of groups.
-
+\textbf{Addition of groups.}
 \TT{add} \EM{optional-flag} \EM{attribute-groups} \TT{in} \EM{av-set}
-\newline
 builds an {\av} set adding the specified \EM{attribute-groups} to each element
 of the given {\av} set.
 If no \EM{flag} is specified the addition is set-theoretic, whereas with the
@@ -115,22 +104,21 @@ considered.
 
 \figref{Add} shows how to build a one-element {\av} set using \TT{add}.
 
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 The set of attributed values given explicitly:
-["head" attr {"attribute-name" = property /"metadata" of "resource"}]
+ ["head" attr {/"attribute" = property /"metadata" of "resource"}]
 
-The same set built with the add operator
-add {"attribute-name" = property /"metadata" of "resource"} in "head"
+The same set built with the add operator:
+ add {/"attribute" = property /"metadata" of "resource"} in "head"
 \end{verbatim} \end{footnotesize}
-\vskip-1pc
+\vspace{-1pc}
 \caption{A simple use of the add operator}
 \label{Add}
 \end{figure}
 
 \item 
-Existential test.
-
+\textbf{Existential test.}
 The existential test has the form \TT{ex} \EM{av-set} where the
 specification of the {\av} set contains some instances of the construction
 \TT{@}\EM{variable}\TT{.}\EM{attribute-name}, and runs as follows:
@@ -138,15 +126,13 @@ the given {\av} set is evaluated replacing each
 \TT{@}\EM{variable}\TT{.}\EM{attribute-name}
 with the contents of \EM{attribute-name} in an attribute group of the {\av}
 stored in \TT{@}\EM{variable} and the evaluation is repeated for every
-possible choice of the groups (recall that different groups are allowed to
+possible choice of these groups (recall that different groups are allowed to
 contain attributes with the same name). If one evaluation gives a non empty
-result, the defaut representation of \emph{true} is returned (the test
-succeded) in the other case the empty {\av} set, {\ie} \emph{false}, is
-returned (the test failed).
+result, the default representation of \emph{true} is returned, in the other
+case the empty {\av} set, {\ie} \emph{false}, is returned.
 
 \item
-Function invocation:
-
+\textbf{Function invocation.}
 The core language allows to invoke two kinds of external functions (with
 which a language extension may be provided): the functions of the first kind 
 return an {\av} set, the functions of the second kind return a piece of 
@@ -156,23 +142,21 @@ code generator). In particular:
 \EM{function-name} \verb+{+ 
 \EM{name} \TT{,} $\cdots$ \TT{,} \EM{name} \verb+} {+
 \EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+
-\newline
-invokes the specified function of the firs kind on the given arguments and
-returns it result. The \EM{name} argument are {\MathQL} paths and usually
+invokes a function of the first kind on the given arguments and returns its
+result. The \EM{name} arguments are {\MathQL} paths and usually
 represent attribute names.
 
 \TT{gen} \EM{function-name} \verb+{+
 \EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+
-\newline
-invokes the specified function of the second kind on the given arguments and
-replaces the function invocation with its result.
+invokes a function of the second kind on the given arguments and replaces
+itself with the function result.
 
-The function names are {\MathQL} paths exactly as the attribute nanes and the 
+The function names are {\MathQL} paths exactly as the attribute names and the 
 graph paths used by the \TT{property} operator. The names of the two kinds of
 functions are kept in distinct environments so they do not clash.
 
 {\MathQL}.4 comes with a basic library of functions of the first kind 
-(see \subsecref{IBasic}) that integrate the core language providing several
-facilities to the user.
+(see \subsecref{Basic}) that integrate the core language providing several
+facilities.
 
 \end{itemize}
diff --git a/helm/mathql/doc/mathql_introduction_property.tex b/helm/mathql/doc/mathql_introduction_property.tex
index f73f5bc78..5fffd7276 100644
--- a/helm/mathql/doc/mathql_introduction_property.tex
+++ b/helm/mathql/doc/mathql_introduction_property.tex
@@ -1,71 +1,67 @@
 \subsection{High level access to metadata} \label{HighAccess}
 
 {\MathQL} high level access to an {\RDF} database is \emph{graph-oriented} and
-is delegated to its \TT{property} operator, that formally accesses an {\RDF}
-graph%
-\footnote
-{When we say {\RDF} graph, we actually mean both the {\RDFM} graph and the
-{\RDFS} graph.}
-through an \emph{access relation} which is better understood by explaining
-the informal semantics of the operator itself.  
-
-This operator builds a \emph{result} {\av} set starting from two mandatory
-arguments: the \emph{source} {\av} set and the \emph{head path}.
+is delegated to its \TT{property} operator that builds a \emph{result} {\av}
+set starting from two mandatory arguments: the \emph{source} {\av} set and the
+\emph{head path}.
 Other optional arguments may be used to change its default behaviour or to
 request advanced functionalities. 
-Its textual syntax is (see \subsecref{Textual}):
+
+This operator has the following syntax, where a path has the structure of an
+attribute name ({\ie} a list of strings) and denotes a (possibly empty) finite
+sequence of contiguous arcs (describing properties in the {\RDF} graph%
+\footnote
+{When we say \emph{{\RDF} graph}, we actually mean both the {\RDFM} graph and
+the {\RDFS} graph.}%
+).
 
 \begin{center}
 \TT{property} \EM{optional-flags} \EM{head-path} \EM{optional-clauses} \TT{of}
 \EM{optional-flag} \EM{av-set}
 \end{center}
 
-A path has the structure of an attribute name ({\ie} a list of strings) and
-denotes a (possibly empty) finite sequence of contiguous arcs (describing
-properties in the {\RDF} graph).
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
-These examples refer to the resources "A" and "B" of Figure 2.
+ These examples refer to the resources "A" and "B" of Figure 2.
 
 Example 1: reading an unstructured property - simple case:
-property "id"/"major" of {"A", "B"}   returns   "1"
-property "id"/"minor" of {"A", "B"}   returns   "2"; "7"
+ property /"id"/"major" of {"A", "B"} gives "1"
+ property /"id"/"minor" of {"A", "B"} gives "2"; "7"
 
 Example 2: reading an unstructured property - use of pattern:
-property "id"/"minor" of pattern ".*"   returns   "2"; "7"
+ property /"id"/"minor" of pattern ".*" gives "2"; "7"
 
 Example 3: reading a structured property without main component:
-property "id" attr "major", "minor" of {"A", "B"}  
-generates the following attributed values:
-"" attr {"major" = "1"; "minor" = "2"}; "" attr {"major" = "1"; "minor" = "7"}
-that are composed using MathQL-1 set-theoretic union giving the one-element set:
-"" attr {"major" = "1"; "minor" = "2"}, {"major" = "1"; "minor" = "7"} 
+ property /"id" attr /"major", /"minor" of {"A", "B"}  
+ generates the following attributed values:
+ "" attr {/"major" = "1"; /"minor" = "2"}; 
+ "" attr {/"major" = "1"; /"minor" = "7"}
+ that are composed with the set-theoretic union giving:
+ "" attr {/"major" = "1"; /"minor" = "2"}, 
+         {/"major" = "1"; /"minor" = "7"} 
 
 Example 4: reading a structured property specifying a main component:
-property "id" main "major" attr "minor" of {"A", "B"}   gives
-"1" attr {"minor" = "2"}, {"minor" = "7"} 
+ property /"id" main /"major" attr /"minor" of {"A", "B"} gives
+ "1" attr {/"minor" = "2"}, {/"minor" = "7"} 
 
 Example 5: the renaming mechanism:
-property "id" attr "minor" as "new-name" of {"A", "B"}   gives  
-"" attr {"new-name" = "2"}, {"new-name" = "7"}
+ property /"id" attr /"minor" as /"new-name" of {"A", "B"} gives  
+ "" attr {/"new-name" = "2"}, {/"new-name" = "7"}
 
 Example 6: imposing constraints on property values:
-property "date" istrue "first" in "2002-01-01" attr "modified" of {"A", "B"}   and  
-property "date" istrue "first" match ".*01.*" attr "modified" of {"A", "B"}    give
-"" attr {"modified" = "2002-03-01"}
-Only the instance of "date" with "first" set to "2002-01-01" is considered.
+ property /"date" istrue /"first" in "2002-01-01" 
+                  attr /"modified" of {"A", "B"} and  
+ property /"date" istrue /"first" match ".*01.*" 
+                  attr /"modified" of {"A", "B"} give
+ "" attr {/"modified" = "2002-03-01"}
+ Only the instance of "date" with "first" set to "2002-01-01" 
+  is considered.
 
 Example 7: inverse traversal of the head path:
-property inverse "date" attr "first" in subj ""   gives
-"A" attr {"first" = "2002-01-01"}; "B" attr {"first" = "2002-02-01"}
-
-Example 8: some triples of an access relation:
-The triples formalizing the property "date" of the resource "A":
-("A", "date", "");
-("A", "date"/"first", "2002-01-01"); ("A", "date"/"modified", "2002-03-01")
+property inverse /"date" attr /"first" in "" gives
+"A" attr {/"first" = "2002-01-01"}; "B" attr {/"first" = "2002-02-01"}
 \end{verbatim} \end{footnotesize}
-\vskip-1pc
+\vspace{-1pc}
 \caption{The ``property'' operator}
 \label{Property}
 \end{figure}
@@ -81,10 +77,9 @@ the query engine, using the resources specified in the head strings of the
 source {\av} set (call them source resources) as start-nodes.
 
 \item
-The computation gives a set of nodes in the {\RDF} graph ({\ie} the end-nodes
-of the instantiated paths) which are the values of the instances of the
-(possibly compound) property specified by the path and concerning the source
-resources.
+The computation gives a set of nodes ({\ie} the end-nodes of the instantiated
+paths) which are the values of the instances of the (possibly compound)
+property specified by the path and concerning the source resources.
 
 \item
 These values, encoded into {\av}'s as explained above, are composed by means
@@ -109,6 +104,7 @@ value's main component in the \TT{main} \EM{optional-clause} (this
 specification overrides the default setting inferred from the {\RDF} graph
 through the \emph{rdf:value} property) and the list of the value's secondary
 components in the \TT{attr} \EM{optional-clause}. 
+
 Note that if a secondary component is not listed in the \TT{attr} clause, it
 will not be read.
 Also recall that, when the result {\av}'s are formed, the main component is
@@ -123,8 +119,9 @@ path.
 Note that the name of an attribute, which by default is its defining path in
 the \TT{attr} clause, can be changed with an optional \TT{as} clause for the
 user's convenience. See for instance \figref{Property} (example 5).
-The alternative could be a simple string but it needs to be a path for typing
-reasons. In any case a string can be seen as a one-element path.
+Note that the assigned name must be a path for typing reasons.
+The alternative could be to use a simple string but in any case a string can
+be seen as a one-element path.
 
 In the default case \TT{property} builds its result considering every
 component of the {\RDFM} graph ({\ie} every {\RDFM}) but we can constrain
@@ -140,7 +137,7 @@ its specification (appearing in the \TT{istrue} or \TT{isfalse} clause) is
 a path in the {\RDF} graph starting from the end-node of the head path.
 
 \TT{property} allows to access the {\RDFS} property hierarchy by specifying
-a flag named \TT{sub} or \TT{super}.
+a flag \TT{sub} or \TT{super}.
 If the \TT{sub} flag is present, \TT{property} inspects the instances of the
 default tree (made by the head path and by the \EM{optional-clauses} paths)
 and every other tree obtained by substituting an arc $ p $ with the arc of a
@@ -160,44 +157,9 @@ component is specified in head strings of the source {\av} set.
 \item
 It encodes the resources corresponding to the instances of the start-nodes into
 {\av}'s assigning the attributes obtained instantiating the attribute paths%
-\footnote{The path in \EM{optional-clauses} are never traversed backward.}
-and composes these {\av}'s using the {\MathQL} set-theoretic union to build
-the result set.
+\footnote{The paths in the \EM{optional-clauses} are never traversed backward.}
+and builds the result set composing these {\av}'s with the set-theoretic union.
 
 \end{enumerate}
 
 See for instance \figref{Property} (example 7).
-
-Now we can present \emph{access relations} which are the formal tools used by
-{\MathQL} semantics to access the {\RDF} graph.
-An access relation is a set of triples $ (r_1, p, r_2) $ where $ r_1 $ and
-$ r_2 $ are strings, $ p $ is a path (encoded as a list of strings). 
-Each triple is a sort of ``extended {\RDF} triple'' in the sense that $ r_1 $
-is is a resource for which metadata is provided, $ p $ is a path in the {\RDF}
-graph and $ r_2 $ is the main value of the end-node of the instance of $ p $
-starting from $ r_1 $ (this includes the instances of sub- and super-arcs of
-$ p $ if necessary).
-See for instance \figref{Property} (example 8).
-
-{\MathQL} does not provide for any built-in access relation so any query
-engine can freely define the access relations that are appropriate with
-respect to the metadata it can access.
-In particular, \secref{Interpreter} describes the access relations implemented
-by the {\HELM} query engine.
-
-It is worth remarking, as it was already stressed in \cite{GS03, Gui03}, that
-the concept of access relation corresponds to the abstract concept of
-property in the basic {\RDF} data model which draws on well established
-principles from various data representation communities.
-In this sense an {\RDF} property can be thought of either as an attribute of a
-resource (traditional attribute-value pairs model), or as a relation between
-a resource and a value (entity-relationship model).
-This observation leads us to conclude that {\MathQL} is sound and complete
-with respect to querying an abstract {\RDF} metadata model. 
-
-Finally note that access relations are close to {\RDF} entity-relationship
-model, but they do not work if we allow paths with an arbitrary number of
-loops ({\ie} with an arbitrary length) because this would lead to creating
-infinite sets of triples.
-If we want to handle this case, we need to turn these relations into
-multivalued functions.
diff --git a/helm/mathql/doc/mathql_introduction_textual.tex b/helm/mathql/doc/mathql_introduction_textual.tex
index 2899a24ce..8e5878bac 100644
--- a/helm/mathql/doc/mathql_introduction_textual.tex
+++ b/helm/mathql/doc/mathql_introduction_textual.tex
@@ -1,6 +1,8 @@
-\subsection{Textual syntax} \label{Textual}
+\section{Textual syntax} \label{Textual}
 
-The syntax of grammatical productions resembles BNF and POSIX notation:
+In this section we present {\MathQL}.4 textual syntax using the same notation
+that we adopted in \cite{GS03,Gui03}. In particular the grammatical
+productions we use resemble {\BNF} with some {\POSIX} formalism:
 
 \begin{itemize}
 
@@ -8,17 +10,13 @@ The syntax of grammatical productions resembles BNF and POSIX notation:
 \TT{::=} defines a grammatical production by means of a regular expression.
 
 Regular expressions are made of the following elements
-(here \TT{...} is a placeholder):
-
-% \item
-% \TT{.} represents any character between U 0020 and U 007F inclusive;
+(\TT{...} is a placeholder):
 
 \item 
 \TT{`...`} represents any character in a character set;
 
 \item 
-\verb+`^ ...`+ represents any character (U+0020 to U+007E) not in a character
-set;
+\verb+`^ ...`+ represents any character (U+20 to U+7E) not in a character set;
 
 \item 
 \TT{"..."} represents a string to be matched verbatim;
@@ -46,13 +44,7 @@ set;
 
 \end{itemize}
 
-\noindent
-{\MathQL} Expressions can contain quoted constant strings with the syntax of
-\figref {StrTS}.%
-\footnote{Note that the first slash of the \GP{path} is not optional as
-in {\MathQL}.3.}
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 <dec>     ::= '0 - 9'
 <num>     ::= <dec> [ <dec> ]*
@@ -65,11 +57,7 @@ in {\MathQL}.3.}
 \caption{Textual syntax of numbers, strings and paths} \label{StrTS}
 \end{figure}
 
-\noindent
-The meaning of the escaped sequences is shown in \figref{EscTS}
-(where $ .... $ is a 4-digit placeholder).
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize}
 \begin{center} \begin{tabular}{|l|l|c|}
 \hline {\bf Escape sequence} & {\bf Unicode character} & {\bf Text} \\
@@ -84,38 +72,43 @@ The meaning of the escaped sequences is shown in \figref{EscTS}
 \caption{Textual syntax of escaped characters} \label{EscTS}
 \end{figure}
 
+Queries and results can contain quoted constant strings with the syntax of
+\figref {StrTS}%
+\footnote
+{Note that the first slash of the \GP{path} is not optional as in {\MathQL}.3.}
+and the meaning of the escaped sequences is shown in \figref{EscTS} (where 
+$ .... $ is a 4-digit placeholder).
 {\MathQL} character escaping syntax aims at complying with W3C character model
 for the World Wide Web \cite{W3Ca} which recommends a support for standard
 Unicode characters (U+0000 to U+FFFF) and escape sequences with start/end
 delimiters.
 In particular {\MathQL} escape delimiters (backslash and caret) are chosen
-among the {\em unwise} characters for URI references (see \cite{URI}) because
-URI references are the natural content of constant strings and these
-characters should not be so frequent in them.
-
-Query expressions can contain variables for {\av}'s (production \GP{avar})
-and variables for {\av} sets, {\ie} for query results (production \GP{svar})
-according to the syntax of \figref{VarTS}.%
-\footnote{This syntax resembles the one of programming languages identifiers.}
+among the \emph{unwise} characters for {\URI} references (see \cite{URI}) 
+because {\URI} references are the natural content of constant strings and 
+these characters should not be so frequent in them.
 
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 <alpha> ::= [ 'A - Z' | 'a - z' | `_` ]+
 <id>    ::= <alpha> [ <alpha> | <dec> ]*
-<avar>  ::= "@" <id>
 <svar>  ::= "$" <id>
+<evar>  ::= "@" <id>
 \end{verbatim}\end{footnotesize} %$
 \vskip-1pc
 \caption{Textual syntax of variables} \label{VarTS}
 \end{figure}
 
-\noindent
-The syntax of query expressions (production \GP{query}) is described in
-\figref{QueryTS}.
+Queries can also contain \emph{set} variables (production \GP{svar}) and
+\emph{element} variables (production \GP{evar}) according to the syntax of
+\figref{VarTS}.%
+\footnote{This syntax resembles the one of programming languages identifiers.}
+A set variable holds an {\av} set, {\ie} a query result, while an element
+variable holds an {\av}.
 
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
-<qualifier> ::= [ "inverse" ]? [ "sub" | "super" ]? <path>
+<ref>       ::= [ "sub" | "super" ]?
+<qualifier> ::= [ "inverse" ]? <ref> <path>
 <main>      ::= [ "main" <path> ]? 
 <cons>      ::= <path> [ "in" | "match" ] <query>
 <istrue>    ::= [ "istrue" <cons> [ "," <cons> ]* ]?
@@ -124,16 +117,16 @@ The syntax of query expressions (production \GP{query}) is described in
 <sec>       ::= [ "attr" <exp> [ "," <exp> ]* ]?
 <opt_args>  ::= <main> <istrue> <isfalses> <sec>
 <source>    ::= [ "pattern" ]? <query>
-<paths>     ::= [ <path> [ "," <path> ]* ]?
+<paths>     ::= <path> [ "," <path> ]*
 <query>     ::= "(" <query> ")" | <string> | "[" <xavs> "]"
             |   "property" <qualifier> <opt_args> "of" <source>
             |   "let" <svar> "=" <query> "in" <query>
-            |   <query> ";;" <query> | <svar> | <avar> 
-            |   "ex" <query> | <avar> "." <path>
-            |   "add" [ "distr" ]? [ <xgroups> | <avar> ] "in" <query>
-            |   "for" <avar> "in" <query> [ "sup" | "inf" ] <query>
+            |   <query> ";;" <query> | <svar> | <evar> 
+            |   "ex" <query> | <evar> "." <path>
+            |   "add" [ "distr" ]? [ <xgroups> | <evar> ] "in" <query>
+            |   "for" <evar> "in" <query> [ "sup" | "inf" ] <query>
             |   "while" <query> [ "sup" | "inf" ] <query>
-            |   <path> "{" <paths> "}" "{" <queries> "}"
+            |   <path> "{" [ <paths> ]? "}" "{" <queries> "}"
             |   "gen" <path> [ "{" <queries> "}" | "in" <query> ] 
 <queries>   ::= [ <query> [ "," <query> ]* ]?
 <xattr>     ::= <path> "=" <query>
@@ -146,11 +139,7 @@ The syntax of query expressions (production \GP{query}) is described in
 \caption{Textual syntax of queries} \label{QueryTS}
 \end{figure}
 
-\noindent
-The syntax of result expressions (production \GP{avs}) is described in
-\figref{ResultTS}.
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 <attr>  ::= <path> "=" <string> | "{" <string> [ "," <string> ]* "}" 
 <group> ::= "{" <attr> [ ";" <attr> ]* "}"
@@ -161,19 +150,29 @@ The syntax of result expressions (production \GP{avs}) is described in
 \caption{Textual syntax of results} \label{ResultTS}
 \end{figure}
 
-The textual syntax of the language extension provided by the basic library
-is in \figref{BasicTS}.
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 <query> ::= "empty" | "false" | "true"
-        |   "not" <query>
-        |   <query> [ "and" | "or" | "xor"| "sub" | "meet" | "eq" | "le"| "lt" ] <query>
-        |   <query> [ "union" | "intersect" ] <query> | { <queries> }  
+        |   [ "not" | "count" | "proj" <path> "of" ] <query>
+        |   <query> [ "and" | "or" | "xor" ] <query>
+        |   <query> [ "sub" | "meet" | "eq" | "le" | "lt" ] <query> 
+        |   <query> [ "union" | "intersect" | "diff" ] <query> 
+        |   "{" <queries> "}"  
+        |   "keep" [ "allbut" ]? [ <paths> "in" ]? <query> 
         |   "if" <query> "then" <query> "else" <query>
-        |   "select" <avar> "from" <query> "where" <query>
+        |   "select" <evar> "from" <query> "where" <query>
 \end{verbatim} \end{footnotesize}
 \vskip-1pc
-\caption{Textual syntax of basic extension} \label{BasicTS}
+\caption{Textual syntax of the basic extension} \label{BasicTS}
 \end{figure}
 
+The core infrastructure of {\MathQL}.4 defines a syntax for queries 
+(\figref{QueryTS}, production \GP{query}) and a syntax for results 
+(\figref{ResultTS}, production \GP{avs}).
+A syntax extension for the most common functions of the basic library is
+also provided for the user's convenience and for backward compatibility with 
+{\MathQL}.3. The syntax extension concerning the functions covered in this
+paper is shown in \figref{BasicTS}.
+Note that this extension makes \GP{avs} an instance of \GP{xavs}.
+
+
diff --git a/helm/mathql/doc/mathql_macros.sty b/helm/mathql/doc/mathql_macros.sty
index 01b563f8d..de81655d4 100644
--- a/helm/mathql/doc/mathql_macros.sty
+++ b/helm/mathql/doc/mathql_macros.sty
@@ -1,9 +1,39 @@
-\usepackage{fguidi-defs} 
+\usepackage{amssymb}
 
-\newcommand{\secref}[1]{Section~\ref{#1}}
-\newcommand{\subsecref}[1]{Subsection~\ref{#1}}
-\newcommand{\figref}[1]{Figure~\ref{#1}}
+\newcommand\CURI[1]{\texttt{<#1>}}
+\newcommand\EM[1]{\noindent\hbox{\frenchspacing\em #1}}
+\newcommand\TT[1]{\noindent\hbox{\frenchspacing\tt #1}}
+\newcommand\RM[1]{\noindent\hbox{\frenchspacing\rm #1}}
+\newcommand\secref[1]{Section~\ref{#1}}
+\newcommand\subsecref[1]{Subsection~\ref{#1}}
+\newcommand\figref[1]{Figure~\ref{#1}}
+\newcommand\ie{{\frenchspacing i.e.}}
+\newcommand\oft{\mathrel :}
+\newcommand\lex{\exists}
+\newcommand\lall{\forall}
+\newcommand\sub{\subseteq}
+\newcommand\meet{\between}
+\newcommand\sand{\cap}
+\newcommand\sdor{\sqcup}
+\newcommand\sor{\cup}
+\newcommand\bigsor{\bigcup}
+\newcommand\app{\mathbin @}
+\newcommand\fa{\phi}
+\newcommand\fb{\psi}
+\newcommand\st{\mathrel |}
+\newcommand\p{{^\prime}}
+\newcommand\jolly{\mathbin\square}
+\newcommand\gdlap[2]{\vbox to 0pt {\vskip#2\hbox{#1}\vss}}
+\newcommand\setnames@[2]{&\gdlap{\kern2pt$#1$}{#2}} 
+\newcommand\imain[1]{{\offinterlineskip\lineskip=2pt\noindent
+  $\vcenter{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}
+\newcommand\iname[1]{\cr\hrulefill\setnames@{#1}{-1.0ex}\cr}
+\newcommand\irule[3]{\imain{#1 \iname{#2} #3}}
+\newcommand\spc{\hspace{1em}}
+\newcommand\icr{\cr}
+\newcommand\Nop{\noindent\hbox to 0pt{\vbox to 1ex{\vfil}\hfil}}
 
+\newcommand\BNF{\textsc{bnf}}
 \newcommand\CAML{\textsc{caml}}
 \newcommand\Galax{\textsc{galax}}
 \newcommand\HELM{\textsc{helm}}
@@ -19,45 +49,49 @@
 \newcommand\XML{\textsc{xml}}
 \newcommand\XQuery{\textsc{xquery}}
 
-\def\av{{\frenchspacing a.v.}}
+\newcommand\av{{\frenchspacing a.v.}}
 
-\def\D{\Delta}
-\def\G{\Gamma}
-\def\ES{\emptyset}
-\def\bigsum{\bigoplus}
-\def\daq{\mathrel{\Downarrow_q}}
-\def\dar{\mathrel{\Downarrow_r}}
-\def\distr{\mathbin\odot}
-\def\dprod{\mathbin\boxtimes} 
-\def\dsum{\mathbin\boxplus} 
-\def\g{(\G_s, \G_a, \G_g)}
-\def\get#1#2{#1(#2)}
-\def\prod{\mathbin\otimes} 
-\def\set#1#2#3{#1[#2 \gets #3]}
-\def\sum{\mathbin\oplus}
+\newcommand\D{\Delta}
+\newcommand\G{\Gamma}
+\newcommand\ES{\emptyset}
+\newcommand\bigsum{\bigoplus}
+\newcommand\daq{\mathrel{\Downarrow_q}}
+\newcommand\dar{\mathrel{\Downarrow_r}}
+\newcommand\distr{\mathbin\odot}
+\newcommand\dprod{\mathbin\boxtimes} 
+\newcommand\dsum{\mathbin\boxplus} 
+\newcommand\g{(\G_s, \G_e, \G_g)}
+\newcommand\get[2]{#1(#2)}
+\newcommand\sdiff{\mathbin\ominus} 
+\newcommand\set[3]{#1[#2 \gets #3]}
+\newcommand\sprod{\mathbin\otimes} 
+\newcommand\ssum{\mathbin\oplus}
 
-\def\Boole{\TT{Boole}}
-\def\Listof{\TT{ListOf}}
-\def\Setof{\TT{SetOf}}
-\def\Str{\TT{String}}
-\def\Num{\TT{Num}}
+\newcommand\Boole{\TT{Boole}}
+\newcommand\Listof{\TT{ListOf}}
+\newcommand\Setof{\TT{SetOf}}
+\newcommand\Str{\TT{Str}}
+\newcommand\Num{\TT{Num}}
 
-\def\All{\TT{All}}
-\def\Exp{\TT{Exp}}
-\def\F{\TT{F}}
-\def\For{\TT{For}}
-\def\Fst{\TT{Fst}}
-\def\Fsts{\TT{Fsts}}
-\def\Fun{\TT{Fun}}
-\def\Gen{\TT{Gen}}
-\def\Istrue{\TT{IsTrue}}
-\def\Match{\TT{Match}}
-\def\Name{\TT{Name}}
-\def\Pattern{\TT{Pattern}}
-\def\Property{\TT{Property}}
-\def\Snd{\TT{Snd}}
-\def\Src{\TT{Src}}
-\def\Unquote{\TT{Unq}}
-\def\T{\TT{T}}
+\newcommand\All{\TT{All}}
+\newcommand\Exp{\TT{Exp}}
+\newcommand\F{\TT{F}}
+\newcommand\For{\TT{For}}
+\newcommand\Fst{\TT{Fst}}
+\newcommand\Fsts{\TT{Fsts}}
+\newcommand\Fun{\TT{Fun}}
+\newcommand\Gen{\TT{Gen}}
+\newcommand\Head{\TT{Head}}
+\newcommand\Istrue{\TT{IsT}}
+\newcommand\Keep{\TT{Keep}}
+\newcommand\Match{\TT{Match}}
+\newcommand\Name{\TT{Name}}
+\newcommand\Pattern{\TT{Pattern}}
+\newcommand\Proj{\TT{Proj}}
+\newcommand\Property{\TT{Property}}
+\newcommand\Snd{\TT{Snd}}
+\newcommand\Src{\TT{Src}}
+\newcommand\Unquote{\TT{Unq}}
+\newcommand\T{\TT{T}}
 
-\def\GP#1{\TT{<#1>}}
+\newcommand\GP[1]{\TT{<#1>}}
diff --git a/helm/mathql/doc/mathql_operational.tex b/helm/mathql/doc/mathql_operational.tex
index 7868d3545..32be697a5 100644
--- a/helm/mathql/doc/mathql_operational.tex
+++ b/helm/mathql/doc/mathql_operational.tex
@@ -5,10 +5,10 @@ operational style \cite{Lan98,Win93}.
 Here we use a simple type system that includes basic types such as strings and
 Booleans, and some type constructors such as product and exponentiation.
 $ y \oft Y $ will denote a typing judgement.
-Note that this semantics is not meant as a formal system \emph{per se}, but
-should serve as a reference for implementors.
+This semantics is not meant as a formal system \emph{per se}, but should be a
+reference for implementors.
 
 \input{mathql_operational_background}
 \input{mathql_operational_core}
-\input{mathql_operational_library}
+\input{mathql_operational_basic}
 
diff --git a/helm/mathql/doc/mathql_operational_background.tex b/helm/mathql/doc/mathql_operational_background.tex
index 0c831f812..ad0be5122 100644
--- a/helm/mathql/doc/mathql_operational_background.tex
+++ b/helm/mathql/doc/mathql_operational_background.tex
@@ -1,33 +1,33 @@
 \subsection {Mathematical background}
 
-As a mathematical background for the semantics, we take the one presented in
-\cite{Gui03}.
+As background for the semantics, we revise the one presented in
+\cite{Gui03,GS03}.
 
 {\Str} denotes the type of strings and its elements are the finite sequences
 of Unicode \cite{Unicode} characters.
-Grammatical productions, represented as strings in angle brackets, denote the
-subtype of {\Str} containing the produced sequences of characters.
+Grammatical productions denote the subtype of {\Str} containing the produced
+sequences of characters.
 
-{\Num} denotes the type of numbers and is the subtype of {\Str} defined by the
-regular expression: \TT{'0 - 9' [ '0 - 9' ]*}.
-In this type, numbers are represented by their decimal expansion.
+{\Num} denotes the type of numbers and is the subtype of {\Str} defined by 
+\GP{num}. In this type, numbers are represented by their decimal expansion.
 
 $ \Setof\ Y $ denotes the type of finite sets ({\ie} unordered finite
-sequences without repetitions) over $ Y $.
+sequences without repetitions) over $ Y $ and
 $ \Listof\ Y $ denotes the type of lists ({\ie} ordered finite sequences)
 over $ Y $.
 We will use the notation $ [y_1, \cdots, y_m] $ for the list whose elements 
-are $ y_1, \cdots, y_m $.
+are $ y_1, \cdots, y_m $ ($ \{y_1, \cdots, y_m\} $ will denote a set as
+usual).
 
-{\Boole}, the type of Boolean values, is defined as
-$ \{\ES, \{("", \ES)\}\} \oft \Setof\ \Setof\ (\Str \times \Setof\ Y) $ 
+{\Boole}, the type of Boolean values, is defined as the set
+$ \{\ES, \{("", \ES)\}\} $ of type $ \Setof\ \Setof\ (\Str \times \Setof\ Y) $ 
 where the first element stands for \emph{false} (denoted by {\F}) and the
-second element stands for \emph{true} (denoted by {\T}).
+second element stands for \emph{true} (denoted by {\T}).%
+\footnote{This definition allows to treat a Boolean value as an {\av} set.}
 
 $ Y \times Z $ denotes the product of the types $ Y $ and $ Z $ whose elements
 are the ordered pairs $ (y, z) $ such that $ y \oft Y $ and $ z \oft Z $.
 The notation is also extended to a ternary product.
-
 $ Y \to Z $ denotes the type of functions from $ Y $ to $ Z $ and $ f\ y $
 denotes the application of $ f \oft Y \to Z $ to $ y \oft Y $.
 Relations over types, such as equality, are seen as functions to {\Boole}.
@@ -55,7 +55,7 @@ $ {\sub} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
 \item
 $ {\meet} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
 
-%\item
+\item
 $ {\sand} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)
 
 \item
@@ -92,17 +92,15 @@ $ U \meet W $ means $ (\lex u \in U)\ u \in W $ and expresses the fact that
 $ U \sand W $ is inhabited as a primitive notion, {\ie} without mentioning
 intersection and equality as for $ U \sand W \neq \ES $, which is equivalent
 but may be implemented less efficiently in real cases%
-\footnote{As for the Boolean condition $ \a \lor \b $ which may have a more
-efficient implementation than $ \lnot(\lnot \a \land \lnot \b) $.}.
-
+\footnote{As for the Boolean condition $ \fa \lor \fb $ which may have a more
+efficient implementation than $ \lnot(\lnot \fa \land \lnot \fb) $.}.
 $ U \meet W $ is a natural companion of $ U \sub W $ being its logical dual
 (recall that $ U \sub W $ means $ (\lall u \in U)\ u \in W $)
 and is already being used successfully in the context of a constructive
 ({\ie} intuitionistic and predicative) approach to point-free topology
 \cite{Sam00}.
 
-Sets of couples play a central role in our formalization and in particular we
-will use:
+Sets of couples play a central role in our presentation and we will use:
 
 \begin{itemize}
 
@@ -125,7 +123,7 @@ This operator has type $ (\Setof\ (Y \times Z)) \to Y \to Z $.
 \item
 Moreover $ \set{W}{y}{z} $ is the set obtained from $ W $ removing every
 couple whose first component is $ y $ and adding the couple $ (y, z) $.
-The type of this operator is \\
+The type of this operator is
 $ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $.  
 
 \item 
diff --git a/helm/mathql/doc/mathql_operational_basic.tex b/helm/mathql/doc/mathql_operational_basic.tex
new file mode 100644
index 000000000..cc309f732
--- /dev/null
+++ b/helm/mathql/doc/mathql_operational_basic.tex
@@ -0,0 +1,298 @@
+\subsection {The basic library}
+
+In this section we present the functions provided by the {\MathQL}.4 basic
+library. Describing the whole library would require an amount of space that
+goes beyond the limits of this paper so we include here just a selection of
+the available functions (the ones for which we gave the syntax extension in
+\secref{Textual}). 
+
+The function below are grouped by their arity.
+
+\begin{itemize}
+
+\item 
+\textbf{The predefined {\av} sets.}
+The functions \TT{/"empty"}, \TT{/"false"} and \newline \TT{/"true"} take no
+path arguments and no set arguments.
+
+\begin{footnotesize} 
+\begin{center} 
+%
+\irule{\Nop}{}{\Fun\ \TT{/"empty"}\ [\,]\ [\,]\ \G \equiv \F} \spc
+\irule{\Nop}{}{\Fun\ \TT{/"false"}\ [\,]\ [\,]\ \G \equiv \F}
+\end{center}  
+\begin{center} 
+%
+\irule{\Nop}{}{\Fun\ \TT{/"true"}\ [\,]\ [\,]\ \G \equiv \T} 
+%
+\end{center} 
+\end{footnotesize}
+
+Moreover ``\TT{empty}'' rewrites to ``\verb+fun /"empty" {} {}+'',
+``\TT{false}'' rewrites to ``\verb+fun /"false" {} {}+'' and
+``\TT{true}'' rewrites to ``\verb+fun /"true" {} {}+''.
+
+\item
+\textbf{Boolean negation and size.}
+The functions \TT{/"not"} and \TT{/"count"} take no path arguments and one set
+argument.
+Here Rule 1 overrides rule 2.
+
+\begin{footnotesize} 
+\begin{center} 
+%
+\irule{(\G, x) \daq \F}{1}{\Fun\ \TT{/"not"}\ [\,]\ [x]\ \G \equiv \T} \spc
+\irule{(\G, x) \daq S}{2}{\Fun\ \TT{/"not"}\ [\,]\ [x]\ \G \equiv \F}
+\end{center}  
+\begin{center} 
+%
+\irule{(\G, x) \daq S}{}{\Fun\ \TT{/"count"}\ [\,]\ [x]\ \G \equiv \#\ S} 
+%
+\end{center} 
+\end{footnotesize}
+
+Moreover ``\TT{not} x'' rewrites to ``\verb+fun /"not" {} {+x\verb+}+''
+and ``\TT{count} x'' rewrites to ``\verb+fun /"count" {} {+x\verb+}+''.
+
+\item 
+\textbf{Boolean xor, set-theoretic and numerical tests, difference.}
+\TT{/"xor"}, \TT{/"sub"}, \TT{/"meet"}, \TT{/"eq"}, \TT{/"le"}, \TT{/"lt"} and
+\TT{/"diff"} take no path arguments and two set arguments.
+The rule with the lowest number is applied first.
+
+\begin{footnotesize} 
+\begin{center} 
+%
+\irule{(\G, x_1) \daq \F \spc (\G, x_2) \daq \F}{1}
+      {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv \T} \spc
+\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq \F}{2}
+      {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv S_1}
+%
+\end{center}  
+\begin{center} 
+%
+\irule{(\G, x_1) \daq \F \spc (\G, x_2) \daq S_2}{3}
+      {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv S_2} \spc
+\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{4}
+      {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv \F}
+%
+\end{center}  
+\begin{center} 
+%
+\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{}
+      {\Fun\ \TT{/"sub"}\ [\,]\ [x_1, x_2]\ \G \equiv (\Fsts\ S_1 \sub \Fsts\ S_2)}
+%
+\end{center}  
+\begin{center} 
+%
+\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{}
+      {\Fun\ \TT{/"meet"}\ [\,]\ [x_1, x_2]\ \G \equiv (\Fsts\ S_1 \meet \Fsts\ S_2)} 
+%
+\end{center} 
+\begin{center} 
+%
+\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{}
+      {\Fun\ \TT{/"eq"}\ [\,]\ [x_1, x_2]\ \G \equiv (\Fsts\ S_1 = \Fsts\ S_2)}
+%
+\end{center} 
+\begin{center} 
+%
+\irule{(\G, x_1) \daq \{(r_1, A_1)\} \spc (\G, x_2) \daq \{(r_2, A_2)\}}{}
+      {\Fun\ \TT{/"le"}\ [\,]\ [x_1, x_2]\ \G \equiv (r_1 \le r_2)}
+%
+\end{center} 
+\begin{center} 
+%
+\irule{(\G, x_1) \daq \{(r_1, A_1)\} \spc (\G, x_2) \daq \{(r_2, A_2)\}}{}
+      {\Fun\ \TT{/"lt"}\ [\,]\ [x_1, x_2]\ \G \equiv (r_1 < r_2)}
+%
+\end{center} 
+\begin{center} 
+%
+\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{}
+      {\Fun\ \TT{/"eq"}\ [\,]\ [x_1, x_2]\ \G \equiv (S_1 \sdiff S_2)}
+%
+\end{center} 
+\end{footnotesize}
+
+where $\sdiff$ is a helper function two rewrite rules:
+
+\begin{footnotesize}
+\begin{center} \begin{tabular}{lrll}
+5 &
+$ (S_1 \sdor \{(r, A_1)\}) \sdiff (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
+$ S_1 \sdiff S_2 $ \\
+6 & $ S_1 \sdiff S_2 $ & rewrites to & $ S_1 $  
+%
+\end{tabular} \end{center}
+\end{footnotesize}
+
+``x \TT{xor} y'' rewrites to ``\verb+fun /"xor" {} {+x\TT{,}y\verb+}+'',
+``x \TT{sub} y'' rewrites to \newline ``\verb+fun /"sub" {} {+x\TT{,}y\verb+}+'',
+``x \TT{meet} y'' rewrites to ``\verb+fun /"meet" {} {+x\TT{,}y\verb+}+'',
+``x \TT{eq} y'' rewrites to ``\verb+fun /"eq" {} {+x\TT{,}y\verb+}+'',
+``x \TT{le} y'' rewrites to \newline ``\verb+fun /"le" {} {+x\TT{,}y\verb+}+'',
+``x \TT{lt} y'' rewrites to ``\verb+fun /"lt" {} {+x\TT{,}y\verb+}+'' and
+``x \TT{diff} y'' rewrites to ``\verb+fun /"diff" {} {+x\TT{,}y\verb+}+''
+
+\item
+\textbf{Conditional operator and standard \emph{select} clause}.
+\TT{/"if"} takes no path arguments and three set arguments.
+The usual rule overriding policy applies.
+
+\begin{footnotesize} 
+\begin{center} 
+%
+\irule{(\G, x_1) \daq \F \spc (\G, x_3) \daq S_3}{1}
+      {\Fun\ \TT{/"if"}\ [\,]\ [x_1, x_2, x_2]\ \G \equiv S_3} \spc
+\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{2}
+      {\Fun\ \TT{/"if"}\ [\,]\ [x_1, x_2, x_2]\ \G \equiv S_2}
+%
+\end{center} 
+\end{footnotesize}
+
+``\TT{if} x \TT{then} y \TT{else} z'' rewrites to
+``\verb+fun /"if" {} {+x\TT{,}y\TT{,}z\verb+}+'' and
+``\TT{select} i \TT{from} x \TT{where} y'' rewrites to
+``\TT{for} i \TT{in} x \TT{sup} \TT{if} y \TT{then} i \TT{else} \TT{empty}''.
+
+\item
+\textbf{Intersection without attribute distribution.}
+\TT{/"intersect"} takes no path arguments and any positive number of set
+arguments.
+
+\begin{footnotesize} 
+\begin{center} 
+%
+\irule{(\G, x_1) \daq S_1 \spc \cdots \spc (\G, x_m) \daq S_m}{}
+      {\Fun\ \TT{/"intersect"}\ [\,]\ [x_1, \cdots, x_m]\ \G \equiv 
+       (S_1 \sprod \cdots \sprod S_m)}
+%
+\end{center} 
+\end{footnotesize}
+
+As usual
+``x \TT{intersect} y'' rewrites to ``\verb+fun /"intersect" {} {+x\TT{,}y\verb+}+''.
+
+\item
+\textbf{Union without attribute distribution, Boolean conjunction and
+disjunction.}
+\TT{/"union"}, \TT{/"and"} and \TT{/"or"} take no path arguments and any
+number of set arguments.
+The usual rule overriding policy applies.
+
+\begin{footnotesize} 
+\begin{center} 
+%
+\irule{\Nop}{}{\Fun\ \TT{/"union"}\ [\,]\ [\,]\ \G \equiv \F} \spc
+\irule{(\G, x_1) \daq S_1 \spc \cdots \spc (\G, x_m) \daq S_m}{}
+      {\Fun\ \TT{/"union"}\ [\,]\ [x_1, \cdots, x_m]\ \G \equiv 
+       (S_1 \ssum \cdots \ssum S_m)}
+%
+\end{center} 
+\begin{center} 
+%
+\irule{\Nop}{}{\Fun\ \TT{/"and"}\ [\,]\ [\,]\ \G \equiv \T} \spc
+\irule{\Nop}{}{\Fun\ \TT{/"or"}\ [\,]\ [\,]\ \G \equiv \F}
+%
+\end{center} 
+\begin{center} 
+%
+\irule{\Fun\ \TT{/"and"}\ [\,]\ l\ \G \equiv \F}{1}
+      {\Fun\ \TT{/"and"}\ [\,]\ (l \app [x])\ \G \equiv \F} \spc
+\irule{\Fun\ \TT{/"or"}\ [\,]\ l\ \G \equiv \F \spc (\G, x) \daq S}{3}
+      {\Fun\ \TT{/"or"}\ [\,]\ (l \app [x])\ \G \equiv S}
+%
+\end{center} 
+\begin{center} 
+%
+\irule{\Fun\ \TT{/"and"}\ [\,]\ l\ \G \equiv S_l \spc (\G, x) \daq S}{2}
+      {\Fun\ \TT{/"and"}\ [\,]\ (l \app [x])\ \G \equiv S} \spc
+\irule{\Fun\ \TT{/"or"}\ [\,]\ l\ \G \equiv S_l}{4}
+      {\Fun\ \TT{/"or"}\ [\,]\ (l \app [x])\ \G \equiv S_l}
+\end{center} 
+\end{footnotesize}
+
+``x \TT{and} y'' rewrites to ``\verb+fun /"and" {} {+x\TT{,}y\verb+}+'',
+``x \TT{or} y'' rewrites to \newline ``\verb+fun /"or" {} {+x\TT{,}y\verb+}+'',
+``x \TT{union} y'' rewrites to \kern-1.1pt ``\verb+fun /"union" {} {+x\TT{,}y\verb+}+''
+and ``\verb+{+x$_1$\TT{,}$\cdots$\TT{,}x$_m$\verb+}+'' rewrites to
+``\verb+fun /"union" {} {+x$_1$\TT{,}$\cdots$\TT{,}x$_m$\verb+}+''.
+
+\item
+\textbf{Projection.}
+\TT{/"proj"} takes one path argument and one set argument.
+
+\begin{footnotesize}
+\begin{center}
+%
+\irule {p \oft \TT{<path>} \spc 
+        (\G, x) \daq \{ (r_1, A_1), \cdots, (r_m, A_m) \}}{}
+       {\Fun\ \TT{/"proj"}\ [p]\ [x]\ \G \equiv 
+        \Head\ (\Proj\ (\Name\ p)\ A_1 \sor \cdots \sor \Proj\ (\Name\ p)\ A_m)}
+%
+\end{center} 
+\begin{center} \begin{tabular}{rll}
+%
+$ \Proj\ p\ \{G_1, \cdots, G_n\} $ & rewrites to &
+$ \get{G_1}{p} \sor \cdots \sor \get{G_n}{p} $ \\
+$ \Head\ \{s_1, \cdots, s_k\} $ & rewrites to & $ \{ (s_1, \ES), \cdots, (s_k, \ES) \} $
+\end{tabular} \end{center}
+\end{footnotesize}
+
+where, for each $ 1 \le j \le n $, $ \get{G_j}{p} $ is $ \ES $ if $ p $ is not
+defined in $ G_j $.
+
+Moreover
+``\TT{proj} p \TT{of} x'' rewrites to ``\verb+fun /"proj" {+p\verb+} {+x\verb+}+''.
+
+\item
+\textbf{Refinement.}
+The functions \TT{/"keep"/"these"} and \TT{/"keep"/"allbut"} take any number
+of path arguments and one set argument.
+In the following rules if $ l $ is $ [p_1, \cdots, p_m] $ then
+$ W $ is $ \{\Name\ p_1, \cdots, \Name\ p_m\} $ Moreover {\Keep} and $\Keep\p$
+are helper functions and the usual rule overriding policy applies.
+
+\begin{footnotesize}
+\begin{center}
+%
+\irule{l \oft \Listof\ \TT{<path>} \spc (\G, x) \daq S}{}
+      {\Fun\ \TT{/"keep"/"these"}\ l\ [x]\ \G \equiv 
+       \{ (r, \bigsor \{ \Keep\ \T\ W\ G \st G \in A \}) \st (r, A) \in S \}}
+%
+\end{center}
+\begin{center}
+%
+\irule{l \oft \Listof\ \TT{<path>} \spc (\G, x) \daq S}{}
+      {\Fun\ \TT{/"keep"/"allbut"}\ l\ [x]\ \G \equiv 
+       \{ (r, \bigsor \{ \Keep\ \F\ W\ G \st G \in A \}) \st (r, A) \in S \}}
+%
+\end{center}
+\begin{center}
+%
+\irule{\Keep\p\ b\ W\ G\ \RM{rewrites to}\ \ES}{1}
+{\Keep\ b\ W\ G\ \RM{rewrites to}\ \ES} \spc
+\irule{\Keep\p\ b\ W\ G\ \RM{rewrites to}\ G\p}{2}
+{\Keep\ b\ W\ G\ \RM{rewrites to}\ \{G\p\}}
+%
+\end{center}
+\begin{center} \begin{tabular}{rll}
+%
+$ \Keep\p\ \T\ W\ G $ & rewrites to & $ \{ (p, V) \in G \st p \in W \} $ \\
+$ \Keep\p\ \F\ W\ G $ & rewrites to & $ \{ (p, V) \in G \st p \notin W \} $
+%
+\end{tabular} \end{center}
+\end{footnotesize}
+
+``\TT{keep} p$_1$\TT{,}$\cdots$\TT{,}p$_m$ \TT{in} x'' rewrites to
+``\TT{fun /"keep"/"these"} \verb+{+p$_1$\TT{,}$\cdots$\TT{,}p$_m$\verb+}+ \verb+{+x\verb+}+'',
+``\TT{keep} x'' rewrites to ``\TT{fun /"keep"/"these"} \verb+{}+ \verb+{+x\verb+}+'',
+``\TT{keep allbut} p$_1$\TT{,}$\cdots$\TT{,}p$_m$ \TT{in} x'' rewrites to
+``\TT{fun /"keep"/"allbut"} \verb+{+p$_1$\TT{,}$\cdots$\TT{,}p$_m$\verb+}+ \verb+{+x\verb+}+''
+and
+``\TT{keep allbut} x'' rewrites to ``\TT{fun /"keep"/"allbut"} \verb+{}+ \verb+{+x\verb+}+''.
+
+Note that ``\TT{keep allbut} x'' gives the same result as ``x'' does.
+
+\end{itemize}
diff --git a/helm/mathql/doc/mathql_operational_core.tex b/helm/mathql/doc/mathql_operational_core.tex
index f9471292b..ed0391752 100644
--- a/helm/mathql/doc/mathql_operational_core.tex
+++ b/helm/mathql/doc/mathql_operational_core.tex
@@ -1,32 +1,32 @@
-\subsection {The core language}
+\subsection {The core language} \label{OCore}
 
 \subsubsection*{Preliminaries}
 
-Wih the above background we are able to type the main objects needed in the
+With the above background we are able to type the main objects needed in the
 formalization:
 
 \begin{itemize}
 
 \item
-A path $ s $ is a list of strings therefore its type is
+A path $ p $ is a list of strings therefore its type is
 $ T_{0a} = \Listof\ \Str $.
 
 \item
-A multiple string value $ V $ is an object of type $ T_{0b} = \Setof\ \Str $.
+The attribute contents $ V $ are an object of type $ T_{0b} = \Setof\ \Str $.
 
 \item
-A attribute group $ G $ is an association set connecting the attribute names
-to their values, therefore its type is
+An attribute group $ G $ is an association set connecting the attribute names
+to their contents, therefore its type is
 $ T_1 = \Setof\ (T_{0a} \times T_{0b}) $. 
 
 \item
-A subject string $ r $ is an object of type $ \Str $.
+A head string $ r $ is an object of type $ \Str $.
 
 \item
 A set $ A $ of attribute groups is an object of type $ T_2 = \Setof\ T_1 $.  
 
 \item
-An {\av} is a subject string with its attribute groups, so its type is
+An {\av}, {\ie} a head string with its attribute groups, has type
 $ T_3 = \Str \times T_2 $. 
 
 \item
@@ -40,8 +40,7 @@ $ T_5 = \Str \times \Str \times (T_{0a} \to \Str) $.
 
 When a constant string appearing in a {\MathQL} expression is unquoted, the
 surrounding double quotes are deleted and each escaped sequence is translated
-according \figref{EscTS}.
-
+according to \figref{EscTS}.
 This operation is formally performed by the function
 $ \Unquote $ of type $ \Str \to \Str $.
 Moreover $ \Name \oft \GP{path} \to T_{0a} $ is a helper function that
@@ -53,14 +52,15 @@ The semantics of {\MathQL} expressions denoting queries is given by the infix
 relation $ \daq $ that evaluates a query to an {\av} set.
 These expressions are evaluated in a context $ \G = \g $
 which is a triple of association sets that connect
-svar's to {\av} sets, avar's to {\av}'s and avar's to attribute groups.
+set variables to {\av} sets, element variables to {\av}'s and element
+variables to attribute groups.
 Therefore the type $ K $ of the context $ \G $ is:
 
 \begin{footnotesize} \begin{center}
 $ 
-\Setof\ (\GP{svar} \times T_4)  \times
-\Setof\ (\GP{avar} \times T_3)\ \times % $ \\ $ \times\
-\Setof\ (\GP{avar} \times T_1)
+\Setof\ (\GP{svar} \times T_4) \times
+\Setof\ (\GP{evar} \times T_3) \times % $ \\ $ \times\
+\Setof\ (\GP{evar} \times T_1)
 $
 \end{center} \end{footnotesize}
 
@@ -73,7 +73,7 @@ $ \mathord{\daq} \oft (K \times \GP{query}) \times (K \times T_4) \to \Boole $.
 \end{tabular} \end{center}
 \end{footnotesize}
 
-The context components $ \G_s $ and $ \G_a $ are used to store the contents of
+The context components $ \G_s $ and $ \G_e $ are used to store the contents of
 variables, while $ \G_g $ is used by the \TT{ex} operator to be presented
 below.
 
@@ -86,15 +86,15 @@ to an {\av} set.
 
 \subsubsection*{Queries}
 
-The first \GP{query} expressions include explicit {\av} sets and syntactic
-grouping:
+The first group of \GP{query} expressions include the representation of
+explicit {\av} sets and the syntactic grouping facility:
 
 \begin{itemize}
 
 \item 
 The syntactic grouping is obtained enclosing a \GP{query} between \TT{(}
 and \TT{)}.    
-An explicit {\av} set can be represented by a single string, which is
+An explicit {\av} set can be represented either by a single string, which is
 converted into a single {\av} with no attributes, or by a \GP{xavs}
 (extended {\av} set) expression enclosed between \TT{[} and \TT{]}.
 Such an expression describes all the components of an {\av} set and is
@@ -110,21 +110,21 @@ evaluated using the rules given below.
 \begin{center} 
 %
 \irule{x_1, \cdots, x_m \in \GP{xav} \spc 
-       (\G, TT{[} x_1 \TT{]}) \daq S_1 \spc \cdots \spc (\G, \TT{[} x_m \TT{]}) \daq S_m}{}
-      {(\G, \TT{[} x_1 \TT{;} \cdots \TT{;} x_m \TT{]}) \daq S_1 \sum \cdots \sum S_m}
+       (\G, \TT{[} x_1 \TT{]}) \daq S_1 \spc \cdots \spc (\G, \TT{[} x_m \TT{]}) \daq S_m}{}
+      {(\G, \TT{[} x_1 \TT{;} \cdots \TT{;} x_m \TT{]}) \daq S_1 \ssum \cdots \ssum S_m}
 %
 \end{center} 
 \begin{center} 
 %
-\irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{xgroup} \spc
+\irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{xgroup} \icr
        (\G, \TT{[} q\ \TT{attr}\ g_1 \TT{]}) \daq S_1 \spc \cdots \spc
        (\G, \TT{[} q\ \TT{attr}\ g_m \TT{]}) \daq S_m}{}
-      {(\G, \TT{[} q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \TT{]}) \daq S_1 \sum \cdots \sum S_m}
+      {(\G, \TT{[} q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \TT{]}) \daq S_1 \ssum \cdots \ssum S_m}
 %
 \end{center} 
 \begin{center} 
 %
-\irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{xatr} \spc
+\irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{xatr} \icr
        (\G, \TT{[} q\ \TT{attr}\ \{ a_1 \} \TT{]}) \daq S_1 \spc \cdots \spc
        (\G, \TT{[} q\ \TT{attr}\ \{ a_m \} \TT{]}) \daq S_m}{}
       {(\G, \TT{[} q\ \TT{attr}\ \{ a_1 \TT{;} \cdots \TT{;} a_m \} \TT{]}) \daq S_1 \dsum \cdots \dsum S_m}
@@ -139,17 +139,16 @@ evaluated using the rules given below.
 \end{center} 
 \end{footnotesize}
 
-$ \dsum $ and $ \sum $ are helper functions describing the two union operations
-on {\av} sets: with and without attribute distribution respectively.
-$ \dsum $ and $ \sum $ have two rewrite rules each.
+$ \dsum $ and $ \ssum $ are helper functions describing the two union
+operations on {\av} sets: with and without attribute distribution respectively.
 
 \begin{footnotesize}
 \begin{center} \begin{tabular}{lrll}
 %
 1a &
-$ (S_1 \sdor \{(r, A_1)\}) \sum (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
-$ (S_1 \sum S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
-1b & $ S_1 \sum S_2 $ & rewrites to & $ S_1 \sor S_2 $ \\ 
+$ (S_1 \sdor \{(r, A_1)\}) \ssum (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
+$ (S_1 \ssum S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
+1b & $ S_1 \ssum S_2 $ & rewrites to & $ S_1 \sor S_2 $ \\ 
 2a &
 $ (S_1 \sdor \{(r, A_1)\}) \dsum (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
 $ (S_1 \dsum S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
@@ -158,14 +157,14 @@ $ (S_1 \dsum S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
 \end{tabular} \end{center}
 \end{footnotesize}
 
-Rules 1a, 2a override 1b, 2b respectively and
-$ A_1 \distr A_2 = \{G_1 \sum G_2 \st G_1 \in A_1, G_2 \in A_2\} $.
+Rules 1a, 2a override 1b, 2b and
+$ A_1 \distr A_2 = \{G_1 \ssum G_2 \st G_1 \in A_1, G_2 \in A_2\} $.
 
 \item 
-The semantics of \TT{property} operator is described below.
+The semantics of the \TT{property} operator is described below.
 
 In the following rule,
-$s$ is ``$ \TT{property}\ h\ p_1\ \TT{main}\ p_2\ \RM{attr}\ e_1, \cdots,
+$s$ is ``$ \TT{property}\ h\ p_1\ \TT{main}\ p_2\ \TT{attr}\ e_1, \cdots,
 e_m\ \TT{in}\ k\ x $'', $P$ is $ \Property\ h $ and
 $A_2$ is $ \{ \Exp\ P\ p_1\ r_1\ \{e_1, \cdots, e_m\}\} $:
 
@@ -173,7 +172,7 @@ $A_2$ is $ \{ \Exp\ P\ p_1\ r_1\ \{e_1, \cdots, e_m\}\} $:
 \begin{center}
 %
 \irule
-{h \oft \GP{refine} \spc p_1, p_2 \oft \GP{path} \spc 
+{h \oft \GP{ref} \spc p_1, p_2 \oft \GP{path} \spc 
  e_1, \cdots, e_m \oft \GP{exp} \spc k \in \TT{["pattern"]?} \spc 
  (\G, x) \daq S
 }{A}
@@ -188,12 +187,17 @@ $A_2$ is $ \{ \Exp\ P\ p_1\ r_1\ \{e_1, \cdots, e_m\}\} $:
 When the \TT{main} clause is not present, we assume $ p_2 = \TT{/} $.
 
 Here $ \Property\ h $ gives the appropriate access relation according to
-the $ h $ flag (this is the primitive function that inspects the {\RDF} graph,
-see \subsecref{HighAccess}). 
-
+the $ h $ flag (this is the primitive function that inspects the {\RDF}
+graph, see \subsecref{HighAccess}).
+ 
 $ \Src\ k\ P\ V $ is a helper function giving the source set
 according to the $ k $ flag. $ \Src $ is based on $ \Match $, the helper
-function handling POSIX regular expressions. Formally:
+function handling {\POSIX} regular expressions.
+Here $ \Pattern\ W\ s $ is the primitive function returning the subset of
+$ W \oft \Setof\ \Str $ whose element match the {\POSIX} 1003.2-1992%
+\footnote{In {\POSIX} 1003.1-2001:
+\CURI{http://www.unix-systems.org/version3/ieee\_\,std.html}.}
+regular expression $ \verb+"^"+ \app s \app \TT{"\$"} $.
 
 \begin{footnotesize}
 \begin{center} \begin{tabular}{rll}
@@ -206,31 +210,22 @@ $ \Match\ W\ V $ & rewrites to & $ \bigsor \{\Pattern\ W\ s \st s \in V\} $
 \end{tabular} \end{center}
 \end{footnotesize}
 
-Here $ \Pattern\ W\ s $ is the primitive function returning the subset of
-$ W \oft \Setof\ \Str $ whose element match the POSIX 1003.2-1992%
-\footnote{Included in POSIX 1003.1-2001:
-\CURI{http://www.unix-systems.org/version3/ieee\_\,std.html}.}
-regular expression $ \verb+"^"+ \app s \app \TT{"\$"} $.
-
-$ \Exp\ P\ \p_1\ r_1\ E $ is the helper function that builds the group of
+$ \Exp\ P\ p_1\ r_1\ E $ is the helper function that builds the group of
 attributes specified in the \TT{attr} clause.
-$ \Exp $ is based on $ \Exp\p $ which handles a single attribute. Formally:
+$ \Exp $ is based on $ \Exp\p $ which handles a single attribute. Formally,
+if $ p, p\p \oft \GP{path} $ and $ E \oft \Setof\ \GP{exp} $:
 
 \begin{footnotesize}
-\begin{center} \begin{tabular}{rlll}
+\begin{center} \begin{tabular}{rll}
 %
 $ f\ P\ r_1\ p_1\ p $ & rewrites to &
-$ \{ r_2 \st (r_1, p_1 \app (\Name\ p), r_2) \in P \} $ &
-with $ p \oft \GP{path} $ \\
+$ \{ r_2 \st (r_1, p_1 \app (\Name\ p), r_2) \in P \} $ \\
 $ \Exp\p\ P\ r_1\ p_1\ p $ & rewrites to &
-$ \{ (\Name\ p, f\ P\ r_1\ p_1\ p) \} $ & 
-with $ p \oft \GP{path} $ \\
+$ \{ (\Name\ p, f\ P\ r_1\ p_1\ p) \} $ \\
 $ \Exp\p\ P\ r_1\ p_1\ (p\ \TT{as}\ p\p) $ & rewrites to &
-$ \{ (\Name\ p\p, f\ P\ r_1\ p_1\ p) \} $ & 
-with $ p, p\p \oft \GP{path} $ \\
+$ \{ (\Name\ p\p, f\ P\ r_1\ p_1\ p) \} $ \\
 $ \Exp\ P\ r_1\ p_1\ E $ & rewrites to &
-$ \bigsum \{ \Exp\p\ P\ r_1\ p_1\ e \st e \in E \} $ &
-with $ E \oft \Setof\ \GP{exp} $ 
+$ \bigsum \{ \Exp\p\ P\ r_1\ p_1\ e \st e \in E \} $ \\ 
 \end{tabular} \end{center}
 \end{footnotesize}
 
@@ -258,7 +253,7 @@ $ (\lall c \in W)\ \Istrue\p\ P\ r_1\ p_1\ c $
 \end{footnotesize}
 
 For each clause ``\TT{isfalse} $ c_1, \cdots, c_n $'' the set $ P $
-must be replaced with
+must be replaced with \newline
 $ \{ (r_1, p, r_2) \in P \st \lnot (\Istrue\ P\ r_1\ p_1\ C) \} $
 (using the above notation).
 Note that these substitutions and the former must be composed if necessary.
@@ -269,8 +264,7 @@ $ \{ (r_2, p, r_1) \st (r_1, p, r_2) \in P \} $.
 
 \end{itemize}
 
-The second group of \GP{query} expressions includes the context manipulation
-facilities:
+The second group of \GP{query} expressions allows the context manipulation:
 
 \begin{itemize}
 
@@ -280,54 +274,53 @@ The operators for reading variables:
 \begin{footnotesize} \begin{center}
 %
 \irule{i \oft \GP{svar}}{}{(\g, i) \daq \get{\G_s}{i}} \spc
-\irule{i \oft \GP{avar}}{}{(\g, i) \daq \{\get{\G_a}{i}\}}
+\irule{i \oft \GP{evar}}{}{(\g, i) \daq \{\get{\G_e}{i}\}}
 %
 \end{center} \end{footnotesize}
 
-$ \get{\G_s}{i} $ and $ \{\get{\G_a}{i}\} $ mean $ \ES $ if $ i $ is not defined.
+$ \get{\G_s}{i} $ and $ \{\get{\G_e}{i}\} $ mean $ \ES $ if $ i $ is not defined.
 
 \item 
-The \TT{let} operator assigns an {\av} set variable (svar):
+The \TT{let} operator assigns a set variable (\GP{svar}):
 
 \begin{footnotesize} 
 \begin{center}
 %
 \irule{i \oft \GP{svar} \spc (\G_1, x_1) \daq (\g, S_1) \spc
-       ((\set{\G_s}{i}{S_1}, \G_a, \G_g), x_2) \daq (\G_2, S_2)}
+       ((\set{\G_s}{i}{S_1}, \G_e, \G_g), x_2) \daq (\G_2, S_2)}
 {}{(\G_1, \TT{let}\ i\ \TT{=}\ x_1\ \TT{in}\ x_2) \daq (\G_2, S_2)} 
 %
 \end{center} 
 \end{footnotesize}
 
 The sequential composition operator \TT{;;} has the semantics of a \TT{let}
-introducing a fresh variable, so ``$ x_1\ \TT{;;}\ x_2 $'' revrites
+introducing a fresh variable, so ``$ x_1\ \TT{;;}\ x_2 $'' rewrites
 to ``$ \TT{let}\ i\ \TT{=}\ x_1\ \TT{in}\ x_2 $'' where $i$ does not occur in
 $x_2$.
 
 \item 
 The \TT{ex} and ``dot'' operators provide a way to read the attributes stored
-in avar's.
-
+in element variables.
 The \TT{ex} (exists) operator gives access to the groups of attributes
-associated to the {\av}'s in the $ \G_a $ part of the context and does
+associated to the {\av}'s in the $ \G_e $ part of the context and does
 this by loading its $ \G_g $ part, which is used by the ``dot'' operator
 described below. 
 
 \TT{ex} is true if the query following it is successful for at least one
-pool of attribute groups, one for each {\av} in the $ \G_a $ part of the
+pool of attribute groups, one for each {\av} in the $ \G_e $ part of the
 context. Formally we have the rules:
 
 \begin{footnotesize}
 \begin{center}
 %
-\irule{(\lall \D_g \in \All\ \G_a)\ ((\G_s, \G_a, \G_g + \D_g), y) \daq \F}
+\irule{(\lall \D_g \in \All\ \G_e)\ ((\G_s, \G_e, \G_g + \D_g), y) \daq \F}
       {1}{(\G, \TT{ex}\ y) \daq \F} \spc
 \irule{\Nop}{2}{(\G, \TT{ex}\ y) \daq \T} \spc
 %
 \end{center}
 \begin{center}
 %
-\irule {i \oft \GP{avar} \spc p \oft \GP{path} \spc \get{\get{\G_g}{i}}{\Name\ p} = \{s_1, \cdots, s_m\}}{}
+\irule {i \oft \GP{evar} \spc p \oft \GP{path} \spc \get{\get{\G_g}{i}}{\Name\ p} = \{s_1, \cdots, s_m\}}{}
        {(\G, i\TT{.}p) \daq \{(s_1, \ES), \cdots, (s_m, \ES)\}}
 %
 \end{center}
@@ -335,31 +328,29 @@ context. Formally we have the rules:
 
 where%
 \footnote{$\D_g$ has the type of $ \G_g $.}
-$ \All\ \G_a = \{\D_g \st \get{\D_g}{i} = G\ \RM{iff}\ G \in \Snd\ \get{\G_a}{i} \} $,
+$ \All\ \G_e = \{\D_g \st \get{\D_g}{i} = G\ \RM{iff}\ G \in \Snd\ \get{\G_e}{i} \} $,
 and $ \G = \g $.
 
 Moreover $ \get{\get{\G_g}{i}}{\Name\ p} $ means $ \ES $
 if $ i $ or $ \Name\ p $ are not defined where appropriate.
-
 Here the first rule has higher precedence than the second one does.
 
 \end{itemize}
 
-The third group of \GP{query} expressions includes the {\av} set manipulation
-facilities:
+The third group of \GP{query} expressions allows the {\av} set manipulation:
 
 \begin{itemize}
 
 \item
 The \TT{add} operator adds a given set of attribute groups to the {\av}'s
 of an {\av} set using a union with or without attribute distribution
-according to the \TT{distr} flag.
+according to the setting of the \TT{distr} flag.
 
 \begin{footnotesize} 
 \begin{center}
 %
 \irule
-{h \in \TT{["distr"]?} \spc a \in \GP{xgroups} \spc 
+{h \in \TT{["distr"]?} \spc a \in \GP{xgroups} \icr 
  (\G, \TT{[} ""\ \TT{attr}\ a \TT{]}) \daq \{("", A)\} \spc 
  (\G, x) \daq \{(r_1, A_1), \cdots, (r_m, A_m)\}}{}
 {(\G, \TT{add}\ a\ \TT{in}\ x) \daq \{(r_1, A_1 \jolly A), \cdots, (r_m, A_m \jolly A)\}}
@@ -368,54 +359,58 @@ according to the \TT{distr} flag.
 \begin{center}
 %
 \irule
-{h \in \TT{["distr"]?} \spc i \in \GP{avar} \spc  
+{h \in \TT{["distr"]?} \spc i \in \GP{evar} \spc  
  (\g, x) \daq \{(r_1, A_1), \cdots, (r_m, A_m)\}}{}
-{(\g, \TT{add}\ i\ \TT{in}\ x) \daq \{(r_1, A_1 \jolly \Snd\ \get{\G_a}{i}), \cdots, (r_m, A_m \jolly \Snd\ \get{\G_a}{i})\}}
+{(\g, \TT{add}\ i\ \TT{in}\ x) \daq \{(r_1, A_1 \jolly \Snd\ \get{\G_e}{i}), \cdots, (r_m, A_m \jolly \Snd\ \get{\G_e}{i})\}}
 %
 \end{center}
 \end{footnotesize}
 
 Where $ \jolly_{\tt""} = \sor $ and $ \jolly_{\tt"distr"} = \distr $.
-Moreover $ \Snd\ \get{\G_a}{i} = \ES $ if $i$ is not defined.
+Moreover $ \Snd\ \get{\G_e}{i} = \ES $ if $i$ is not defined.
 
 \item
-The semantics of the \TT{for} operator is given in terms of the {\For} helper
+The semantics of the \TT{for} operator is given using the {\For} helper
 function:
 
 \begin{footnotesize}
 \begin{center}
 %
-\irule{i \oft \GP{avar} \spc (\G, x_1) \daq (\G_1, S_1) \spc h \in \TT{["sup"|"inf"]}}
-{}{(\G, \TT{for}\ i\ \TT{in}\ x_1\ h\ x_2) \daq \For\ h\ \G_1\ i\ x_2\ S_1} \spc
-\irule{i \oft \GP{avar} \spc x_2 \oft \GP{query}}{}
+\irule{i \oft \GP{evar} \spc (\G, x_1) \daq (\G_1, S_1) \spc h \in \TT{["sup"|"inf"]}}
+{}{(\G, \TT{for}\ i\ \TT{in}\ x_1\ h\ x_2) \daq \For\ h\ \G_1\ i\ x_2\ S_1}
+%
+\end{center} 
+\begin{center}
+%
+\irule{i \oft \GP{evar} \spc x_2 \oft \GP{query}}{}
       {\For\ h\ \G\ i\ x_2\ \ES\ \RM{rewrites to}\ (\G, \ES)}
 %
 \end{center} 
 \begin{center}
 %
-\irule{i \oft \GP{avar} \spc ((\G_s, \set{\G_a}{i}{R}, \G_g), x_2) \daq (\G_2, S_2)}
+\irule{i \oft \GP{evar} \spc ((\G_s, \set{\G_e}{i}{R}, \G_g), x_2) \daq (\G_2, S_2)}
       {}{\For\ h\ \G\ i\ x_2\ (S_1 \sdor \{R\})\ \RM{rewrites to}\
       (\G_2 ,(\Snd\ (\For\ h\ \G_2\ i\ x_2\ S_1)) \jolly_h S_2)} 
 %
 \end{center}
 \end{footnotesize}
 
-Here we have $ R \oft T_3 $, $ \G = \g $, $ \jolly_{\tt"sup"} = \sum $ and
-$ \jolly_{\tt"inf"} = \prod $.
+Here we have $ R \oft T_3 $, $ \G = \g $, $ \jolly_{\tt"sup"} = \ssum $ and
+$ \jolly_{\tt"inf"} = \sprod $.
 
-$ \dprod $ and $ \prod $ are helper functions describing the two intersection
+$ \dprod $ and $ \sprod $ are helper functions describing the two intersection
 operations on {\av} sets: with and without attribute distribution respectively.
-They are dual to $ \dsum $ and $ \sum $. $ \dprod $ does not appear in this
-version of {\MathQL} but was used in the erlier versions 
-\cite{Lor02, GS03, Gui03}.   
+They are dual to $ \dsum $ and $ \ssum $. $ \dprod $ does not appear in this
+version of {\MathQL} but was used in the earlier versions 
+\cite{Lor02,GS03,Gui03}.   
 
 \begin{footnotesize}
 \begin{center} \begin{tabular}{lrll}
 %
 1a &
-$ (S_1 \sdor \{(r, A_1)\}) \prod (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
-$ (S_1 \prod S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
-1b & $ S_1 \prod S_2 $ & rewrites to & $ \ES $ \\ 
+$ (S_1 \sdor \{(r, A_1)\}) \sprod (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
+$ (S_1 \sprod S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
+1b & $ S_1 \sprod S_2 $ & rewrites to & $ \ES $ \\ 
 2a &
 $ (S_1 \sdor \{(r, A_1)\}) \dprod (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
 $ (S_1 \dprod S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
@@ -424,7 +419,7 @@ $ (S_1 \dprod S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
 \end{tabular} \end{center}
 \end{footnotesize}
 
-As for $ \sum $ and $ \dsum $, rules 1a, 2a override rules 1b, 2b respectively.
+As for $ \ssum $ and $ \dsum $, rules 1a, 2a override rules 1b, 2b respectively.
 
 \item
 The semantics of the \TT{while} operator is given by the rules below:
@@ -440,20 +435,19 @@ The semantics of the \TT{while} operator is given by the rules below:
 %
 \irule
 {h \in \TT{["sup"|"inf"]} \spc (\G, x_1) \daq (\G_1, S_1) \spc
- (\G_1, x_2) \daq (\G_2, S_2) \spc 
+ (\G_1, x_2) \daq (\G_2, S_2) \icr 
  (\G_2, \TT{while}\ x_1\ h\ x_2) \daq (\G_3, S)}{2}
 {(\G, \TT{while}\ x_1\ h\ x_2) \daq (\G_3, S_2 \jolly_h S)}
 %
 \end{center} 
 \end{footnotesize}
 
-Again $ \jolly_{\tt"sup"} = \sum $ and $ \jolly_{\tt"inf"} = \prod $.
-Moreover rule 1 takes precedence over rule 2.
+Again $ \jolly_{\tt"sup"} = \ssum $ and $ \jolly_{\tt"inf"} = \sprod $.
+Rule 1 takes precedence over rule 2.
 
 \end{itemize}
 
-The forth group of \GP{query} constructions make {\MathQL} an extensible
-language.
+The forth group of \GP{query} constructions makes {\MathQL} extensible.
 
 \begin{itemize}
 
@@ -482,7 +476,7 @@ The core language does not include any external function and it is a mistake
 to invoke an undefined function.
 
 \item
-The \TT{gen} construction invokes an external function returning a \GP{query}
+The \TT{gen} construction invokes an external function returning a \GP{query}.
 The function is identified by a \GP{path} and its arguments are a set of 
 \GP{query}'s. It is a mistake to invoke a function with the wrong number of
 \GP{query}'s as input (each particular function defines this number
@@ -503,24 +497,21 @@ where $ \Gen \oft \GP{path} \times (\Listof\ \GP{query}) \times K \to
 \GP{query} $ is the primitive function performing the low level invocation. 
 The core language does not include any external function of this kind and it
 is a mistake to invoke an undefined function.
-
-The construction ``\TT{gen} p \TT{in} x'' rewrites to ``\TT{gen} p \{x\}''
-for the user's convenience.
+The construction ``\TT{gen} p \TT{in} x'' rewrites to ``\TT{gen} p \{x\}''.
 
 \end{itemize}
 
 \subsubsection*{Results}
 
-An \GP{avs} expression ({\ie} the explicit representation of an {\av} set that
-can denote a query result) is evaluated to an {\av} set according to the
-following rules.
+An \GP{avs} expression (the explicit representation of an {\av} set denoting a
+query result) is evaluated to an {\av} set according to the following rules.
 
 \begin{footnotesize}
 \begin{center} 
 %
 \irule{x_1, \cdots, x_m \in \GP{av} \spc 
        x_1 \dar S_1 \spc \cdots \spc x_m \dar S_m}{}
-      {x_1 \TT{;} \cdots \TT{;} x_m \dar S_1 \sum \cdots \sum S_m}
+      {x_1 \TT{;} \cdots \TT{;} x_m \dar S_1 \ssum \cdots \ssum S_m}
 %
 \end{center} 
 \begin{center} 
@@ -528,7 +519,7 @@ following rules.
 \irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{group} \spc
        q\ \TT{attr}\ g_1 \dar S_1 \spc \cdots \spc
        q\ \TT{attr}\ g_m \dar S_m}{}
-      {q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \dar S_1 \sum \cdots \sum S_m}
+      {q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \dar S_1 \ssum \cdots \ssum S_m}
 %
 \end{center} 
 \begin{center} 
@@ -541,6 +532,13 @@ following rules.
 \end{center} 
 \begin{center} 
 %
+\irule{q, q_0 \in \GP{string} \spc p \in \GP{path}}{}
+      {q\ \TT{attr}\ \{ p = q_0 \} \dar 
+       \{(\Unquote\ q, \{ \{ (\Name\ p, \{ \Unquote\ q_0 \}) \} \})\}}
+%
+\end{center} 
+\begin{center} 
+%
 \irule{q, q_1, \cdots, q_m \in \GP{string} \spc p \in \GP{path}}{}
       {q\ \TT{attr}\ \{ p = \{ q_1 \TT{,} \cdots \TT{,} q_m \} \} \dar 
        \{(\Unquote\ q, \{ \{ (\Name\ p, \{ \Unquote\ q_1, \cdots, \Unquote\ q_m \}) \} \})\}}
diff --git a/helm/mathql/doc/mathql_overview.tex b/helm/mathql/doc/mathql_overview.tex
index 6d59b55fa..45fd2cb99 100644
--- a/helm/mathql/doc/mathql_overview.tex
+++ b/helm/mathql/doc/mathql_overview.tex
@@ -16,7 +16,6 @@ database or on-line libraries reviewers, for proof assistants or
 proof-checking systems, and also for learning environments because these
 applications require features for classifying, searching and browsing
 mathematical information in a semantically meaningful way.
-
 Other languages to be defined in the context of the MathQL proposal may be
 suitable for queries about the semantic structure of mathematical data:
 this includes content-based pattern-matching and possibly other forms of
@@ -50,6 +49,8 @@ native support for post-processing the query results;
 We will briefly analyze these features in the remaining part of this
 section.
 
+\vspace{-1pc}
+
 \subsubsection*{The main requirements from the RDF community}
 
 As a query language for {\RDF} databases, {\MathQL} has a well-conceived
@@ -66,9 +67,8 @@ part of a solution should be preserved, and supports a machine-processable
 the best usability.
 The two syntaxes concern both queries and results, making {\MathQL} usable in
 a distributed environment where query engines are implemented as stand-alone
-components. This is because in this setting both queries and query results
-must be exchanged by the system's components and thus need to be encoded in
-clearly defined format.
+components. In this setting in fact both the queries and their results must be
+exchanged by the system's components and thus need to be clearly encoded.
 
 {\MathQL} provides a graph-oriented access to the {\RDF} metadata, based on
 tree instantiation.
@@ -80,9 +80,11 @@ definitely desirable especially in a distributed context.
 {\MathQL} query results are meant to capture the structure of trees coming
 from an {\RDF} graph and for this purpose a standard $1$- or $2$-dimensional
 organization (as provided by most {\RDF}-oriented query languages) is not
-satisfactory. Here {\MathQL} approach is to use a $4$-dimensional organization
+satisfactory. {\MathQL} approach is to use a $4$-dimensional organization
 for its query results.
 
+\vspace{-1pc}
+
 \subsubsection*{Post-processing and code generation capabilities}
 
 The {\MathQL} query engine, that is written in {\CAML}%
@@ -112,7 +114,6 @@ Moreover the language provides access to an extensible set of code-generating
 functions (also available at {\CAML} side) that the expert user can define
 writing suitable {\CAML} modules for the engine.
 Note that the generated code is always {\MathQL} code.
-
 The code generation features allow to build complex queries incrementally and
 in an automatic manner, as required by the needs of the {\HELM} project.
 Using the native programming language, instead, queries can include the
@@ -123,6 +124,8 @@ In this sense the alternative of performing a complex query on a remote
 component issuing some {\MathQL} querying code followed by some {\CAML}
 post-processing code is really infeasible in a distributed context.  
 
+\vspace{-1pc}
+
 \subsubsection*{Physical organization of the RDF database}
 
 The implementation of the {\MathQL} query engine does not depend on any
diff --git a/helm/mathql/doc/mathql_tests.tex b/helm/mathql/doc/mathql_tests.tex
new file mode 100644
index 000000000..1e31b9472
--- /dev/null
+++ b/helm/mathql/doc/mathql_tests.tex
@@ -0,0 +1,28 @@
+\section{A use case: retrieving the transitive principles} 
+
+In this section we briefly present one on the many queries that we are using
+to test {\MathQL}.4: the one that retrieves the transitive principles stored
+in the {\HELM} library. The details on the {\RDF} metadata used to index the
+contents of the library can be found in \cite{Sch02,Gui03,GSC03}.
+This query, executed in {\MySQL}-mode on an AMD Athlon 1.5 GHz, retrieved 
+$55$ {\HELM} objects (out of $41451$) in $4.00s$ (the interpreter worked
+for $0.31s$) after having issued $2205$ {\SQL} queries to the underlying
+database. This test was executed on April 2 2004 by the Author.
+
+\begin{footnotesize} \begin{verbatim}
+gen /"helm"/"aliases" in let $sets = property inverse /"refSort" istrue 
+/"h:sort" in $SET, /"h:position" in $MC, /"h:depth" in "0" of "" in let
+$prop = property inverse /"refSort" istrue /"h:sort" in $PROP, 
+/"h:position" in $MC, /"h:depth" in "2" of "" in let $rels0 = for @uri
+in $prop sup add {/"set" = property /"refObj" main /"h:occurrence" istrue
+/"h:position" in $MH of @uri} in @uri in let $rels = select @uri from
+$rels0 where ex ((count @uri./"set" eq "1") and (@uri./"set" sub $sets))
+in let $trans0 = for @uri in $rels sup add {/"rel" = @uri; /"set" = proj
+/"set" of @uri} in property inverse /"refObj" main /"h:occurrence" istrue
+/"h:position" in $MC, /"h:depth" in "5" of @uri in let $trans1 = for @uri
+in $trans0 sup add distr {/"premises" = property /"refObj" main /"h:occur
+rence" istrue /"h:position" in $MH of @uri; /"extra" = property /"refObj"
+main /"h:occurrence" istrue /"h:position" in {$IC, $IH} of @uri} in @uri
+in let $trans = select @uri from $trans1 where ex (not @uri./"extra" and
+(@uri./"premises" sub {@uri./"rel", @uri./"set"})) in keep $trans
+\end{verbatim} \end{footnotesize} %$
-- 
2.39.2