\batchmode

                          













  

             

   

   











































 


















\documentclass[twoside,10pt]{article}
\makeatletter
\usepackage{fancyhdr}
\textwidth=12.6truecm
\topmargin=1truecm
\oddsidemargin=1.4truecm
\evensidemargin=1.9truecm
\setcounter{page}{0}

\hyphenation{ref-lec-ti-on}


\newcommand {\oo}{[\kern -.13 em [}

\newcommand {\cc}{]\kern -.13 em ]}

\newcommand {\milord}{{\sl \bf Mi\-lord~II}}

\newcommand {\milordold}{{\sl Mi\-lord}}

\newcommand {\terapia}{{\sl Te\-rap--IA}}

\newcommand {\spongia}{{\sl Spon\-g--IA}}

\newcommand {\bacteria}{{\sl Bact\-er--IA}}

\newcommand {\pneumonia}{{\sl Pneu\-mon--IA}}

\newcommand {\pneumoniatwo }{{\sl Pneu\-mon--IA~II}}

\newcommand {\renoir}{{\sl Renoir}}

\newcommand {\ensai }{{\sl Ens--AI}}

\newcommand {\gtepia }{{\sl Gtep--IA}}

\newcommand {\iiia}{{\sl IIIA}}

\newcommand {\myfigure}[3]
   {\begin{figure}[tbhp]
    \begin{center}
   {#3}
   \end{center}
   \caption{#2}
   \label{#1}
   \end{figure}}

\newcommand {\figurecod}[3]
   {\begin{figure}[tbhp]
    \requadrar{
xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxxxxxx\kill
    #3}
    \caption{#2} \label{#1} \end{figure}}

\newcommand {\dibuix}[3]
{\vbox to #2
  {\hrule width #1 height 0pt depth 0pt
   \vfill
   \special{picture #3}}}

\newcommand {\extfigure}[3]
  {\begin{figure}[tbhp]
    \centerline{#3}
    \caption{#2}
    \label{#1}
    \end{figure}}

\newcommand {\mytable}[3]
   {\begin{table}[tbhp]
    \begin{center}
   {#3}
   \end{center}
   \caption{#2}
   \label{#1}
   \end{table}}

\newcommand {\lineofcode}[1]
   {\begin{quote}
     	  {\tt #1}
   \end{quote}}

\newcommand {\claus}[2]
      {$#1 = \left\{\begin{array}{ll}
             #2 \end{array} \right. $}

\newcommand {\linealone}[1]
   {\begin{quote}
     	  {#1}
   \end{quote}}

\newcommand {\inter}[2]
   {[{\it #1},{\it #2}]}

\newcommand {\ovdash}{\vdash_{\cal O}}

\newcommand {\mvdash}{\vdash_{\cal M}}

\newcommand {\omodels}{\models_{\cal O}}

\newcommand {\mmodels}{\models_{\cal M}}

\newcommand {\mrule}[4]
   { {\it {#1}:} {\bf If} {#2} {\bf then conclude} {#3} {\bf is} ${#4}$ }

\newcommand {\mfact}[2]
   { {\it {#1}} {\bf is} {#2} }

\newcommand {\mneg}[1]
	  { {\bf no} ({#1}) }

\newcommand {\nuple}[1]{\langle#1\rangle}

\newcommand {\ub}[1]{{\bf \underline{#1}}}

\newcommand {\ubpo}{{\bf \underline{(}}}

\newcommand {\ubpc}{{\bf \underline{)}}}

\newcommand {\ubp}[1]{{\bf \underline{(}} #1 {\bf \underline{)}}}

\newcommand {\ubq}[1]{{\bf \underline{[}} #1 {\bf \underline{]}}}

\newcommand {\sem}[1]{\mbox{\oo#1\cc}}

\newcommand {\semst}[1]
{\begin{tabbing}
 xxxxxx\= \kill #1 \end{tabbing}}

\newcommand {\stat}[2]{[#1 \mapsto #2]}

\newcommand {\bregla}[2]
   {{\bf If} {#1} {\bf then conclude} {#2}}

\newcommand {\regla}[3]
   {{\bf If} {#1} {\bf then conclude} {#2} {\bf is} {\it {#3}}}

\newcommand {\fet}[2]
   {{\it {#1}} {\bf is} {\it {#2}}}

\newcommand {\negat}[1]
	  { {\bf no} ({#1}) }

\newcommand {\conj}[2]
	  {{#1} {\bf and} {#2}}

\newcommand {\comentari}[1]
   {\fbox{\bf \large #1!!}}

\newcommand {\requadrar}[1]
   {\begin{center}\fbox{\begin{minipage}{1cm}
                  \small
                  \begin{tabbing}
                  #1
                  \end{tabbing}
   \end{minipage}} \end{center}}

\def\gem{\discretionary {l-}{l}{l\mbox{$\,\cdot$}l}}

\newcommand {\ors}
 {\mbox{$\vert$ }}

\newcommand {\itemsy}[2]
 {#1 \> ::= \> #2 \\ }

\newcommand {\litemsy}[2]
 {#1 \> ::= \> #2}

\newcommand {\iitemsy}[2]
 {#1 \> ::= \> #2 $\vert$ \\ }

\newcommand {\nitemsy}[1]
 {\> \> #1 $\vert$ \\ }

\newcommand {\fitemsy}[1]
 {\> \> #1 \\ }

\newcommand {\lfitemsy}[1]
 {\> \> #1}

\newcommand {\syntax}[1]
 {\requadrar{xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill
  #1}}

\newcommand {\newsyntax}[3]
   {\begin{figure}[tbh]
    \begin{center}
   \syntax{#3}
   \end{center}
   \caption{#2}
   \label{#1}
   \end{figure}}

\newcommand {\plusy}[1]
 {$\mbox{#1}^+$}

\newcommand {\timesy}[1]
 {$\mbox{#1}^*$}

\newcommand {\wsyntax}[1]
   {\small
    \begin{tabbing}
    xxxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill
    #1
   \end{tabbing}}

\def\x#1#2#3#4#5#6#7\relax{\def  \x{#1#2#3#4#5#6}}

\def\y{splain}

\def\x{\endgroup\@setsize\SetFigFont{#2pt}}

\renewcommand {\headrulewidth}{0pt}

\makeatother
\newenvironment{tex2html_wrap}{}{}
\newwrite\lthtmlwrite
\def\lthtmltypeout#1{{\let\protect\string\immediate\write\lthtmlwrite{#1}}}%
\newbox\sizebox
\begin{document}
\pagestyle{empty}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$A_8$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6196: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\setcounter{page}{0}
{\newpage
\clearpage
\samepage % latex2html id marker 6198
\thepage
}

\stepcounter{section}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\vert$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6199: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6201: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \begin{tabular}{ll} \\ 
        L ::= R       & The syntax of L is defined by R \\ 
   \mbox{[ X ] }      & An optional item \\ 
\mbox{X $\vert$ Y }   & An item from one of the syntactic categories X or Y\\ 
$\mbox{X}^+$             & One or more occurrences of the syntactic category X
 \end{tabular}
}

\stepcounter{section}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


PROGRAM \> ::= \> $\mbox{moddecl}^+$ \\ 

moddecl \> ::= \> {\bf \underline{Module}} {\it amodid} [{\bf \underline{=}} bodyexpr] \\ 

bodyexpr \> ::= \> {\bf \underline{begin}} decl {\bf \underline{end}} \mbox{$\vert$ } pathid \\ 

pathid \> ::= \> {\it amodid} \mbox{$\vert$ } {\it amodid}{\bf \underline{/}}pathid \\ 

decl \> ::= \> [hierarchy] [interface] [deductive] [control] \\ 

hierarchy \> ::= \> moddecl \mbox{$\vert$ } hierarchy hierarchy \\ 

interface \> ::= \> [{\bf \underline{Import}} predicateidlist] 
                   [{\bf \underline{Export}} predicateidlist] \\ 

predicateidlist \> ::= \> {\it predid} {\bf \underline{,}} predicateidlist \mbox{$\vert$ } {\it 
predid} 
\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{module1}
\end{figure}
}

\stepcounter{section}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill

deductive \> ::= \> {\bf \underline{Deductive knowledge}} \\ 
    \> \> [{\bf \underline{Dictionary:}} [{\bf \underline{Types:}} $\mbox{typebinding}^+$]
       [{\bf \underline{Predicates:}} $\mbox{predicate}^+$] \\ 
    \> \> [{\bf \underline{Rules:}} $\mbox{rule}^+$] \\ 
    \> \> [{\bf \underline{Inference system:}} logcomp] \\ 
    \> \> {\bf \underline{end deductive}} \\ 

typebinding \> ::= \> {\it typeid} [{\bf \underline{=}} typespec]

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{deduck}
\end{figure}
}

\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


predicate \> ::= \> {\it predid} {\bf \underline{=}} attributes \\ 

attributes \> ::= \> [name] [question] type [function] [$\mbox{relation}^+$]
                    [explanation] [image] \\  

name \> ::= \> {\bf \underline{Name:}} {\it string} \\ 

question \> ::= \> {\bf \underline{Question:}} {\it string} \\ 

type \> ::= \> {\bf \underline{Type:}} typespec \\ 

function \> ::= \> {\bf \underline{Function:}}  {\bf \underline{(}} S-expression {\bf \underline{)}} \\ 

relation \> ::= \> {\bf \underline{Relation:}} relationid pathpredid \\ 

pathpredid \> ::= \> pathid{\bf \underline{/}}{\it predid} \mbox{$\vert$ } {\it predid} \\ 

relationid \> ::= \> {\bf \underline{Needs}} \mbox{$\vert$ } {\bf \underline{Needs\_true}}
              \mbox{$\vert$ } {\bf \underline{Needs\_false}} \mbox{$\vert$ } {\bf \underline{Needs\_value}} $\vert$ \\ 
     \> \> {\bf \underline{Belongs\_to}} \mbox{$\vert$ } {\bf \underline{Needs\_quantitative}} 
              \mbox{$\vert$ } {\bf \underline{Needs\_qualitative}} \mbox{$\vert$ } {\it symbol} \\ 

explanation \> ::= \> {\bf \underline{Explanation:}} {\it string} \\ 

image \> ::= \> {\bf \underline{Image:}} {\it fileid}

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{facts}
\end{figure}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


typespec \> ::= \> {\bf \underline{boolean}} \mbox{$\vert$ } {\bf \underline{many-valued}} \mbox{$\vert$ }
                   {\bf \underline{numeric}} \mbox{$\vert$ } {\bf \underline{class}} $\vert$ \\  \> \> {\bf \underline{fuzzy}}
      char-funct \mbox{$\vert$ } {\bf \underline{(}} symbollist {\bf \underline{)}} \mbox{$\vert$ } {\bf \underline{(}} valuesspec {\bf \underline{)}} \mbox{$\vert$ } {\it
      typeid} \\ 

symbollist \> ::= \> {\it symbol}  [{\it string}] \mbox{$\vert$ }
        symbollist {\bf \underline{,}} symbollist \\ 

valuesspec \> ::= \> {\it symbol}  [{\it string}] char-funct \mbox{$\vert$ }
        valuesspec {\bf \underline{,}} valuesspec \\ 

char-funct \> ::= \> {\bf \underline{(}} {\it number} {\bf \underline{,}}
       {\it number} {\bf \underline{,}} {\it number} {\bf \underline{,}} {\it number} {\bf \underline{)}}


\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{types}
\end{figure}
}

{\newpage
\clearpage
\samepage \begin{figure}[tbhp]
\centerline{\begin{picture}(260,117)(160,625)
\thicklines
\put(180,640){\vector( 0, 1){ 80}}
\put(180,640){\vector( 1, 0){240}}
\thinlines
\multiput(175,700)(8.06452,0.00000){16}{\line( 1, 0){  4.032}}
\multiput(300,700)(0.00000,-7.64706){9}{\line( 0,-1){  3.824}}
\put(260,645){\line( 0,-1){ 10}}
\multiput(300,700)(0.00000,-7.64706){9}{\line( 0,-1){  3.824}}
\put(300,645){\line( 0,-1){ 10}}
\put(375,645){\line( 0,-1){ 10}}
\put(270,640){\line( 0, 1){ 0}} 
\put(175,640){\line( 1, 0){ 10}}
\put(175,650){\line( 1, 0){ 10}} 
\put(175,660){\line( 1, 0){ 10}}
\put(175,700){\line( 1, 0){ 10}}
\thicklines
\put(260,640){\line( 2, 3){ 40}}
\put(300,700){\line( 1, 0){80}}
\put(155,640){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$a_0$}}}
\put(155,650){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$a_1$}}}
\put(155,660){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$a_2$}}}
\put(155,670){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$\cdots$}}}
\put(155,695){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$a_{n-1}$}}}
\put(160,730){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$\mu_{fever} 
(temperature)$}}}
\put(410,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$temperature$}}}
\put(175,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$0^\circ$}}}
\put(255,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$37^\circ$}}}
\put(295,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$38^\circ$}}}
\put(370,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$43^\circ$}}}
\end{picture}
}

\label{fuzzy}
\end{figure}
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mu_{treatment}(etambutol)=[\alpha,\beta]$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6287: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \begin{figure}[tbhp]
\centerline{\begin{picture}(255,95)(165,625)
\thicklines
\put(180,640){\vector( 0, 1){ 80}}
\put(180,640){\vector( 1, 0){240}}
\thinlines
\multiput(175,700)(8.07018,0.00000){25}{\line( 1, 0){  4.035}}
\put(260,645){\line( 0,-1){ 10}}
\put(300,645){\line( 0,-1){ 10}}
\put(375,645){\line( 0,-1){ 10}}
\put(340,645){\line( 0,-1){ 10}}
\multiput(300,640)(0.00000,8.00000){8}{\line( 0, 1){  4.000}}
\multiput(320,640)(0.00000,8.00000){8}{\line( 0, 1){  4.000}}
\multiput(340,645)(0.00000,8.46154){7}{\line( 0, 1){  4.231}}
\multiput(285,640)(0.00000,8.00000){8}{\line( 0, 1){  4.000}}
\multiput(270,700)(0.00000,-8.00000){8}{\line( 0,-1){  4.000}}
\put(270,640){\line( 0, 1){  0}}
\put(175,640){\line( 1, 0){ 10}}
\put(175,650){\line( 1, 0){ 10}}
\put(175,660){\line( 1, 0){ 10}}
\put(175,700){\line( 1, 0){ 10}}
\thicklines
\put(260,640){\line( 1, 6){ 10}}
\put(270,700){\line( 1, 0){ 15}}
\put(285,700){\line( 1,-4){ 15}}
\put(285,640){\line( 1, 4){ 15}}
\put(300,700){\line( 1, 0){ 20}}
\put(320,700){\line( 1,-3){ 20}}
\put(320,640){\line( 1, 3){ 20}}
\put(340,700){\line( 1, 0){ 35}}
\put(155,640){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$a_0$}}}
\put(155,650){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$a_1$}}}
\put(155,660){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$a_2$}}}
\put(155,670){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$\cdots$}}}
\put(155,695){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$a_{n-1}$}}}
\put(410,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$temperature$}}}
\put(175,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$0^\circ$}}}
\put(255,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$37^\circ$}}}
\put(295,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$38^\circ$}}}
\put(270,705){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$\mu_{low}$}}}
\put(335,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$39^\circ$}}}
\put(370,625){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$43^\circ$}}}
\put(375,705){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$\mu_{high}$}}}
\put(315,705){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{rm}$\mu_{medium}$}}}
\end{picture}
}

\label{f:enum}
\end{figure}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


S-expression \> ::= \> {\it atom} \mbox{$\vert$ } list \mbox{$\vert$ } predef-func
\mbox{$\vert$ } S-expression S-expression \\ 

list \> ::= \> {\bf \underline{(}} S-expression {\bf \underline{)}} \mbox{$\vert$ } {\bf \underline{(}}  {\bf \underline{)}} \\ 

predef-func \> ::= \> {\bf \underline{(}} {\bf \underline{Type}} {\it predid} {\bf \underline{)}} \mbox{$\vert$ } 
                     {\bf \underline{(}} {\bf \underline{Linguistic\_terms}} {\bf \underline{)}}

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{function}
\end{figure}
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$etiq\_1 \preceq
etiq\_2$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6329: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\preceq$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6331: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \begin{displaymath}clearance\_of\_creatinina = 140 - \frac{age \times weight \times
        \left\{ \begin{array}{ll}
                   1.0 & \mbox{if {\it male}} \\ 
                   0.8 & \mbox{if {\it female}}
                \end{array}
        \right\}}{72}\end{displaymath}
}

\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


rule \> ::= \> {\it ruleid} {\bf \underline{If}} premisse-rule {\bf \underline{Then}}
                          conclusion-rule [{\it documentation}] \\ 

premisse-rule \> ::= \> condition-rule {\bf \underline{and}} premisse-rule \mbox{$\vert$ }
                        condition-rule \\ 

condition-rule \> ::= \> conditio \mbox{$\vert$ } {\bf \underline{no}} {\bf \underline{(}} conditio {\bf \underline{)}} \\ 

conditio \> ::= \> operator {\bf \underline{(}} expression{\bf \underline{,}} ...{\bf \underline{,}} expression {\bf \underline{)}} $\vert$ \\ 
             \> \> expression operator expression $\vert$ \\ 
             \> \> pathpredid \mbox{$\vert$ } {\it ltermid} \mbox{$\vert$ } {\bf \underline{true}} 
                                 \mbox{$\vert$ } {\bf \underline{false}} \\ 

expression \> ::= \> operator-arit {\bf \underline{(}} expression{\bf \underline{,}} ...{\bf \underline{,}} 
                          expression {\bf \underline{)}} $\vert$ \\ 
              \> \> {\bf \underline{(}} expression operator-arit expression {\bf \underline{)}} $\vert$ \\ 
              \> \> {\it number} \mbox{$\vert$ } pathpredid \\ 

operator \> ::= \> {\bf \underline{$<$}} \mbox{$\vert$ } {\bf \underline{$>$}} \mbox{$\vert$ } {\bf \underline{$<=$}} \mbox{$\vert$ }
               {\bf \underline{$>=$}} \mbox{$\vert$ } {\bf \underline{=}} \mbox{$\vert$ } {\bf \underline{/=}} \mbox{$\vert$ } {\bf \underline{int}} $\vert$ \\ 

operator-arit \> ::= \> {\bf \underline{+}} \mbox{$\vert$ } {\bf \underline{-}} \mbox{$\vert$ } {\bf \underline{*}} \mbox{$\vert$ } {\bf \underline{:}} \\ 

conclusion-rule \> ::= \> {\bf \underline{conclude}} rconclusion {\bf \underline{is}} cert-value \\ 

rconclusion \> ::= \> {\it predid} \mbox{$\vert$ }
                 {\it predid} {\bf \underline{=}} {\it symbol} \mbox{$\vert$ }
            {\bf \underline{no}} {\bf \underline{(}} {\it predid} {\bf \underline{)}} \mbox{$\vert$ }
                 {\bf \underline{no}} {\bf \underline{(}} {\it predid} {\bf \underline{=}} {\it symbol} {\bf \underline{)}}

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{rules}
\end{figure}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\alpha \in A_n$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6401: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$[\alpha, \alpha]$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6403: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \begin{mytable}{table3}{Arithmetic operations between expressions.}
{\begin{tabular}{|l||l|l|}\cline{2-3} \cline{2-3}
  \multicolumn{1}{c}{} &
  \multicolumn{1}{|c|}{\bf numeric} &
  \multicolumn{1}{c|}{\bf set}                  \\  \hline \hline

  {\tt a + b} &  
  $a + b$                        & 
  $A \cup B$                         \\  \hline
  
  {\tt a - b} &  
  $a - b$                        & 
  no sense                        \\  \hline
  
  {\tt a * b} &  
  $a \times b$                        & 
  $A \cap B$                           \\  \hline
  
  {\tt a :~b} &  
  $a \div b$                        & 
  no sense                        \\  \hline \hline
\end{tabular}}
\end{mytable}
}

{\newpage
\clearpage
\samepage \begin{mytable}{oper}{Operations between expressions.}
{\begin{tabular}{|l||l|l|}\cline{2-3} \cline{2-3}
  \multicolumn{1}{c}{} &
  \multicolumn{1}{|c|}{\bf numeric} &
  \multicolumn{1}{c|}{\bf set}                  \\  \hline \hline

  {\tt a < b} &  
  $a < b$                        & 
  $A \tilde{\subset} B$                         \\  \hline
  
  {\tt a > b} &  
  $a > b$                        & 
  $A \tilde{\supset} B$                        \\  \hline
  
  {\tt a <= b} &  
  $a \leq b$                        & 
  $A \tilde{\subseteq} B$                         \\  \hline
  
  {\tt a >= b} &  
  $a \geq b$                        & 
  $A \tilde{\supseteq} B$                        \\  \hline
  
  {\tt a = b}  &  
  $a = b$                        & 
  $A \tilde{=} B$                         \\  \hline

  {\tt a /= b} &  
  $a \neq b$                         & 
  $A \tilde{\neq} B$                        \\  \hline

  {\tt a int b} &  
  no sense                        & 
  $A \tilde{\cap} B \neq \emptyset$                 \\  \hline \hline
\end{tabular}}
\end{mytable}
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mu^{fever}_{high}(s)$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6459: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$max(\mu^{fever}_{medium}(t),\mu^{fever}_{high}(t)).$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6463: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\stepcounter{subsubsection}
\stepcounter{section}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


logcomp \> ::= \> [lingtermdef] [conjunction] [renaming] \\ 

lingtermdef \> ::= \> {\bf \underline{Truth values =}} {\bf \underline{(}} ltermidlist {\bf \underline{)}} \\ 

ltermidlist \> ::= \> {\it ltermid} {\bf \underline{,}} ltermidlist \mbox{$\vert$ } {\it ltermid} \\ 

conjunction \> ::= \> {\bf \underline{Conjunction}} {\bf \underline{=}} truth-table \\ 

truth-table \> ::= \> {\bf \underline{Truth table}} {\bf \underline{(}} arrows {\bf \underline{)}} \\ 

arrows \> ::= \> {\bf \underline{(}} termlist {\bf \underline{)}} \mbox{$\vert$ } arrows arrows \\ 

renaming \> ::= \> {\bf \underline{Renaming}} $\mbox{lrenames}^+$ \\ 

lrenames \> ::= \> pathid{\bf \underline{/}}{\it ltermid} {\bf \underline{==$>$}} cert-value \\ 

cert-value \> ::= \> {\it ltermid} \mbox{$\vert$ }
         {\bf \underline{[}}  {\it ltermid} {\bf \underline{,}} {\it ltermid} {\bf \underline{]}}

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{logics}
\end{figure}
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$A_n = a_0 \preceq a_1 \preceq \cdots \preceq a_{n-1}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6477: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$a_0$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6479: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$a_{n-1}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6481: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$B_7$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6487: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$A_5$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6489: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\stepcounter{section}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


gexpr \> ::= \> {\it predid} {\bf \underline{(}} term
                         {\bf \underline{,}} ... {\bf \underline{,}} term {\bf \underline{)}} \\ 

term \> ::= \> {\it {\bf \underline{\$}}varid} \mbox{$\vert$ } {\it symbol} \mbox{$\vert$ } 
               {\it termid}(term, ..., term)

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{deccon2}
\end{figure}
}

{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


mexpr \> ::= \> known \mbox{$\vert$ } mrel \mbox{$\vert$ } msubmod \mbox{$\vert$ } mthres \mbox{$\vert$ } card \mbox{$\vert$ }
              atom \mbox{$\vert$ } member $\vert$ \\ 
        \> \> eqdif \mbox{$\vert$ } moper \mbox{$\vert$ } int \mbox{$\vert$ }
              setof \mbox{$\vert$ } pos \mbox{$\vert$ } gexpr \\ 

symorvar \> ::= \> {\it symbol} \mbox{$\vert$ } {\bf \underline{\$}}{\it symbol} \\ 

vpath \> ::= \> symorvar \mbox{$\vert$ } symorvar{\bf \underline{/}}vpath \\ 

known \> ::= \> {\bf \underline{K}} {\bf \underline{(}} fact, interval {\bf \underline{)}} \\ 

fact \> ::= \> factex \mbox{$\vert$ } {\bf \underline{not}}{\bf \underline{(}} factex {\bf \underline{)}} \mbox{$\vert$ } 
             {\bf \underline{implies}}{\bf \underline{(}} list{\bf \underline{,}}list {\bf \underline{)}} \\ 

factex \> ::= \> vpath \mbox{$\vert$ } {\bf \underline{=}}{\bf \underline{(}} vpath, symorvar {\bf \underline{)}} \\ 

interval \> ::= \> {\it {\bf \underline{\$}}symbol} 
              \mbox{$\vert$ } {\bf \underline{int}}{\bf \underline{(}} symorvar, symorvar {\bf \underline{)}} \\ 

mrel \> ::= \> {\it relationid}{\bf \underline{(}} symorvar, vpath {\bf \underline{)}} \\ 

msubmod \> ::= \> {\bf \underline{submodule}}{\bf \underline{(}} symorvar, symorvar {\bf \underline{)}} \mbox{$\vert$ }
                  {\bf \underline{submodule}}{\bf \underline{(}} symorvar {\bf \underline{)}} \\ 

mthres \> ::= \> {\bf \underline{threshold}}{\bf \underline{(}} symorvar, symorvar {\bf \underline{)}} \mbox{$\vert$ }
                  {\bf \underline{threshold}}{\bf \underline{(}} symorvar {\bf \underline{)}} \\ 

card \> ::= \> {\bf \underline{cardinal}}{\bf \underline{(}} list, symorvar {\bf \underline{)}} \\ 

list \> ::= \> {\bf \underline{\$}}{\it listid} \mbox{$\vert$ } {\bf \underline{(}} listelem {\bf \underline{)}} \\ 

listelem \> ::= \> {\it elemid} \mbox{$\vert$ } {\it elemid} {\bf \underline{,}} listelem \\ 

atom \> ::= \> {\bf \underline{atom}}{\bf \underline{(}} list {\bf \underline{)}} \\ 

member \> ::= \> {\bf \underline{member}} {\bf \underline{(}} symorvar, list {\bf \underline{)}} \\ 

eqdif \> ::= \> {\bf \underline{equal}}{\bf \underline{(}} listorsym,listorsym {\bf \underline{)}} \mbox{$\vert$ } 
               {\bf \underline{diff}}{\bf \underline{(}} listorsym,listorsym {\bf \underline{)}} \\ 

listorsym \> ::= \> symbol \mbox{$\vert$ } list \\ 

moper \> ::= \> loper{\bf \underline{(}} symorvar,symorvar {\bf \underline{)}} \\ 

loper \> ::= \> {\bf \underline{lt}} \mbox{$\vert$ } {\bf \underline{le}} \mbox{$\vert$ } {\bf \underline{eq}} \mbox{$\vert$ } {\bf \underline{neq}} \mbox{$\vert$ } 
               {\bf \underline{ge}} \mbox{$\vert$ } {\bf \underline{gt}} \\ 

int \> ::= \> {\bf \underline{intersection}}{\bf \underline{(}} list,list {\bf \underline{)}} \\ 

setof \> ::= \> {\bf \underline{set\_of\_instances}}
                     {\bf \underline{(}} {\bf \underline{\$}}{\it var},term,{\bf \underline{\$}}{\it var} {\bf \underline{)}} \\ 

pos \> ::= \> {\bf \underline{position}}{\bf \underline{(}} symorvar,list,symorvar {\bf \underline{)}}

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{metapred}
\end{figure}
}

\stepcounter{subsubsection}
\stepcounter{subsubsection}
\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$amodid^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6583: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$cert\_value$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6589: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\stepcounter{section}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


control \> ::= \> {\bf \underline{Control knowledge}} \\ 
   \> \> [{\bf \underline{Evaluation type:}} evaltype] \\ 
   \> \> [{\bf \underline{Truth threshold:}} {\it ltermid}] \\ 
   \> \> [deduccnt] [structcnt] \\ 
 \> \> {\bf \underline{end control}} \\ 

evaltype \> ::= \> {\bf \underline{lazy}} \mbox{$\vert$ } {\bf \underline{eager}} \mbox{$\vert$ } {\bf \underline{reified}}

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{f:control}
\end{figure}
}

\stepcounter{subsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$a_2$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6601: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$A_n$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6603: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\stepcounter{subsection}
\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\wedge$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6631: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\neg$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6635: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


deduccnt \> ::= \> {\bf \underline{Deductive control:}} $\mbox{mrr}^+$ \\ 

mrr \> ::= \> metaid {\bf \underline{If}} premisse-meta {\bf \underline{Then}} $\mbox{filter-mrr}^+$ \\ 

premisse-meta \> ::= \> mexpr {\bf \underline{and}} premisse-meta
            \mbox{$\vert$ } mexpr \\ 

filter-mrr \> ::= \> {\bf \underline{inhibit rules}} [relation-id] pathpredid $\vert$ \\ 
            \> \> {\bf \underline{prune}} pathpredid \mbox{$\vert$ } {\bf \underline{conclude}} gexpr
                      \mbox{$\vert$ } {\bf \underline{conclude}} known    

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{deccon}
\end{figure}
}

\stepcounter{subsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


structcnt \> ::= \> {\bf \underline{Structural control:}} $\mbox{mre}^+$ \\ 

mre \> ::= \> metaid {\bf \underline{If}} premisse-meta {\bf \underline{Then}} filter-mre \\ 

filter-mre \> ::= \> {\bf \underline{filter}} $\mbox{amodid}^+$ $\vert$ \\ 
          \> \> {\bf \underline{order}} $\mbox{amodid}^+$  {\bf \underline{with certainty}} cert-value $\vert$ \\ 
          \> \> {\bf \underline{Open}} {\bf \underline{(}} term {\bf \underline{)}} \mbox{$\vert$ } {\bf \underline{Module}} {\bf \underline{(}} term {\bf \underline{)}}
                   \mbox{$\vert$ } {\bf \underline{Inherit}} {\bf \underline{(}} \it amodid {\bf \underline{)}} \\ 

mrx \> ::= \> metaid {\bf \underline{If}} premisse-meta {\bf \underline{Then}} exception \\ 

exception \> ::= \> {\bf \underline{definitive solution}} predid $\vert$ \\ 
          \> \> {\bf \underline{stop}}

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{strcon}
\end{figure}
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\$z$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6699: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$[\$min,\$max]$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6703: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\$min$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6705: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\$cut$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6709: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$Refinement\_method$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6717: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$DM/\$z$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6719: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\stepcounter{section}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


PROGRAM \> ::= \> $\mbox{moddecl}^+$ \\ 

moddecl \> ::= \> {\bf \underline{Module}} {\it amodid} [{\bf \underline{(}} [paramlist] {\bf \underline{)}}] 
                 [{\bf \underline{=}} bodyexpr] \\ 

bodyexpr \> ::= \> {\bf \underline{begin}} decl {\bf \underline{end}}
                   \mbox{$\vert$ } pathid [{\bf \underline{(}} [iparamlist] {\bf \underline{)}}] \\ 

paramlist \> ::= \> {\it amodid} {\bf \underline{;}} paramlist \mbox{$\vert$ } 
                    {\it amodid} \\ 

iparamlist \> ::= \> bodyexpr {\bf \underline{;}} iparamlist \mbox{$\vert$ } 
                    bodyexpr 

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{genericmod}
\end{figure}
}

\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


PROGRAM \> ::= \> $\mbox{moddecl}^+$ \\ 

moddecl \> ::= \> {\bf \underline{Module}} {\it amodid} [{\bf \underline{(}} [paramlist] {\bf \underline{)}}]
                 [modoper modexpr]
                 [{\bf \underline{=}} modexpr] \\ 

modexpr \> ::= \> bodyexpr modoper modexpr \mbox{$\vert$ } bodyexpr \\ 

paramlist \> ::= \> paramlist {\bf \underline{;}} paramlist \mbox{$\vert$ } 
                    {\it amodid} modoper modexpr \\ 

iparamlist \> ::= \> modexpr {\bf \underline{;}} iparamlist \mbox{$\vert$ } 
                    modexpr \\ 

modoper \> ::= \> {\bf \underline{:}} \mbox{$\vert$ } {\bf \underline{$>$}} \mbox{$\vert$ } {\bf \underline{$<$}} 

\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{opermod}
\end{figure}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\equiv$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6757: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\stepcounter{subsubsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{figure}[tbh]
\begin{center}
\begin{center}\fbox{\begin{minipage}{1cm}
\small
\begin{tabbing}
xxxxxxxxxxxxx\=xxx\=xxxxxxxxxxxx\kill


hierarchy \> ::= \> moddecl \mbox{$\vert$ }
        {\bf \underline{Inherit}} {\it modid} \mbox{$\vert$ }
        {\bf \underline{Open}} bodyexpr \mbox{$\vert$ }
        hierarchy hierarchy
 
\end{tabbing}
\end{minipage}} \end{center}
\end{center}

\label{synsub}
\end{figure}
}

\stepcounter{section}
{\newpage
\clearpage
\samepage \begin{figure}[tbhp]
\begin{center}
{
\setlength{\unitlength}{0.92pt} \begin{picture}(293,175)
       \thicklines
              \put(190,63){\it Communication}
              \put(267,38){\vector(-1,0){78}}
              \put(189,54){\vector(1,0){78}}
              \put(21,150){\bf MODULE}
              \put(10,10){\framebox(257,160){}}
       \thinlines
              \put(60,85){\it Reflection}
              \put(169,85){\it Reification}
              \put(117,107){\vector(0,-1){42}}
              \put(155,65){\vector(0,1){42}}
              \put(82,30){\framebox(107,35){\bf Deduction}}
              \put(82,107){\framebox(107,35){\bf Meta-deduction}}
\end{picture}}
\end{center}

\label{concy}
\end{figure}
}

\stepcounter{subsection}
\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{displaymath}Query: Module \times Query \rightarrow Query \times Value\end{displaymath}
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$q = sm/q_{sm}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6781: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$Query(sm,q_{sm})$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6785: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{displaymath}Eval: Fact \rightarrow Fact \times Value\end{displaymath}
}

{\newpage
\clearpage
\samepage \begin{displaymath}Eval(f) = \mbox{\tt loop } \{Update(Search(f)); \mbox{ \tt if } value(f)
\mbox{ \tt return } (f,value(f))\}\end{displaymath}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{displaymath}Search: Fact \rightarrow Fact \times Value\end{displaymath}
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$f = sm/f_{sm}$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6821: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$Query(sm,f_{sm})$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6825: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{displaymath}Update: State \times Fact \times Value
          \rightarrow State \times (Fact \times Value)^*\end{displaymath}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$A,A
\rightarrow B \vdash B$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6867: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$(A \wedge B) \rightarrow C \equiv A \rightarrow (B
\rightarrow C)$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6869: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$A,A \wedge B \rightarrow C \vdash B \rightarrow C$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6871: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$B \rightarrow C$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6873: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$A
\wedge B \rightarrow C$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6875: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$A \wedge B
\wedge C \rightarrow D$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6879: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$B \rightarrow D$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6885: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\alpha$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6901: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\rho$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6903: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \begin{displaymath}(A,\alpha), (A \wedge B \rightarrow C,
\rho) \vdash (B \rightarrow C, \rho')\end{displaymath}
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\rho'=
conjunction(\alpha,\rho) $}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6907: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \begin{displaymath}Specialization: Rule^* \times (Fact \times Value)^* \rightarrow
                  Rule^* \times (Fact \times Value)^*\end{displaymath}
}

\stepcounter{subsection}
\stepcounter{subsection}
\stepcounter{section}
\appendix
\stepcounter{section}
{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{moddecl}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6917: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{typebinding}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6945: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{predicate}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6947: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{rule}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6949: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{relation}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline6969: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{ltermid}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline7053: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{lrenames}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline7057: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{mrr}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline7067: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{filter-mrr}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline7069: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{mre}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline7079: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

{\newpage
\clearpage
\samepage \setbox\sizebox=\hbox{$\mbox{amodid}^+$}\lthtmltypeout{latex2htmlSize :tex2html_wrap_inline7081: \the\ht\sizebox::\the\dp\sizebox.}\box\sizebox
}

\stepcounter{section}
{\newpage
\clearpage
\samepage \begin{displaymath}A_8 = \{gp, mpop, llp, modp, p, fp, mp, s\}\end{displaymath}
}

{\newpage
\clearpage
\samepage \begin{mytable}{table2}{Conjunction table for $A_8$.}
{\begin{tabular}{|r||r|r|r|r|r|r|r|r|} \cline{2-9} \cline{2-9}
  \multicolumn{1}{c}{$T_8$} &
  \multicolumn{1}{||r|}{gp} &
  \multicolumn{1}{|r|}{mpop} &
  \multicolumn{1}{|r|}{llp} &
  \multicolumn{1}{|r|}{modp} &
  \multicolumn{1}{|r|}{p} &
  \multicolumn{1}{|r|}{fp} &
  \multicolumn{1}{|r|}{mp} &
  \multicolumn{1}{r|}{s}                  \\  \hline \hline

  gp                        & 
  gp                        &  
  gp                        & 
  gp                        &
  gp                        &
  gp                        &
  gp                        &
  gp                        &
  gp                        \\  \hline
  
  mpop                        &  
  gp                &  
  mpop                   & 
  mpop                &
  mpop                &
  mpop                &
  mpop                &
  mpop                &
  mpop                \\  \hline
  
  llp                        &  
  gp                &  
  mpop                   & 
  mpop                &
  llp                &
  llp                &
  llp                &
  llp                &
  llp                \\  \hline

  modp                        &  
  gp                     &  
  mpop                   & 
  llp                &
  modp                &
  modp                          &
  modp                          &
  modp                          &
  modp                          \\  \hline
  
  p                        &  
  gp                     &  
  mpop                   & 
  llp                &
  modp                &
  modp                          &
  modp                          &
  p                          &
  p                    \\  \hline
  
  fp                        &  
  gp                     &  
  mpop                   & 
  llp                &
  modp                &
  modp                          &
  p                          &
  fp                          &
  fp                    \\  \hline
  
  mp                        &  
  gp                     &  
  mpop                   & 
  llp                &
  modp                &
  p                          &
  fp                    &
  mp                    &
  mp                          \\  \hline

  s                        &  
  gp                     &  
  mpop                   & 
  llp                &
  modp                &
  p                          &
  fp                    &
  mp                    &
  s                          \\  \hline
\end{tabular}}
\end{mytable}
}

\stepcounter{section}

\end{document}
