1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc/mat-eng.tex Thu Apr 17 18:01:02 2003 +0200
1.3 @@ -0,0 +1,1713 @@
1.4 +%In the following this text is not compatible with isac-code:
1.5 +%* move termorder to knowledge: FIXXXmat0201a
1.6 +%
1.7 +%
1.8 +
1.9 +\documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}
1.10 +\usepackage{latexsym} % recommended by Ch.Schinagl 10.98
1.11 +\bibliographystyle{alpha}
1.12 +
1.13 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.14 +
1.15 +\title{\isac --- Interface for\\
1.16 + Developers of Math Knowledge\\[1.0ex]
1.17 + and\\[1.0ex]
1.18 + Tools for Experiments in\\
1.19 + Symbolic Computation\\[1.0ex]}
1.20 +\author{The \isac-Team\\
1.21 + \tt isac-users@ist.tugraz.at\\[1.0ex]}
1.22 +\date{\today}
1.23 +
1.24 +\begin{document}
1.25 +\maketitle
1.26 +\newpage
1.27 +\tableofcontents
1.28 +\newpage
1.29 +\listoftables
1.30 +\newpage
1.31 +
1.32 +\section{Introduction}
1.33 +\subsection{The scope of this document}
1.34 +\paragraph{As a manual:} This document describes the interface to \isac's kernel (KE), the interface to the mathematics engine (ME) included in the KE, and to the various tools like rewriting, matching etc.
1.35 +
1.36 +\isac's KE is written in SML, the language developed in conjunction with predecessors of the theorem prover Isabelle. Thus, in this document we use the plain ASCII representation of SML code. The reader may note that the \isac-user is presented a completely different view on a graphical user interface.
1.37 +
1.38 +The document is selfcontained; basic knowledge about SML (as an introduction \cite{Paulson:91} is recommended), terms and rewriting is assumed.
1.39 +
1.40 +%The interfaces will be moderately exended during the first phase of development of the mathematics knowledge. The work on the subprojects defined should {\em not} create interfaces of any interest to a user or another author of knowledge except identifiers (of type string) for theorems, rulesets etc.
1.41 +
1.42 +Notation: SML code, directories, file names are {\tt written in 'tt'}; in particular {\tt ML>} is the KE prompt.
1.43 +
1.44 +\paragraph{Give it a try !} Another aim of this text is to give the reader hints for experiments with the tools introduced.
1.45 +
1.46 +\subsection{Related documents}\label{related-docs}
1.47 +Isabelle reference manual \cite{Isa-ref}, also contained in the Isabelle distribution under $\sim${\tt /doc/}.
1.48 +
1.49 +{\bf The actual locations of files is being recorded in \\{\tt /software/services/isac/README}
1.50 +\footnote{The KEs current version is {\tt isac.020120-math/} which is based on the version Isabelle99 at {\tt http://isabelle.in.tum.de}.\\
1.51 +The current locations at IST are\\
1.52 +{\tt [isabelle]\hspace{3em} /software/sol26/Isabelle99/}\\
1.53 +{\tt [isac-src]\hspace{3em} /software/services/isac/src/ke/}\\
1.54 +{\tt [isac-bin]\hspace{3em} /software/services/isac/bin/ke/}
1.55 +}
1.56 +and rigorously updated.} In this document we refer to the following directories
1.57 +\begin{tabbing}
1.58 +xxx\=Isabelle sources1234 \=\kill
1.59 +\>Isabelle sources \> {\tt [isabelle]/}\\
1.60 +\>KE sources \> {\tt [isac-src]/\dots{version}\dots/}\\
1.61 +\>KE binary \> {\tt [isac-bin]/\dots{version}\dots/}
1.62 +\end{tabbing}
1.63 +where {\tt\dots version\dots} stands for a directory-name containing information on the version.
1.64 +
1.65 +\subsection{Getting started}
1.66 +Change to the directory {\tt [isac-bin]} where \isac's binary is located and type to the unix-prompt '$>$' (ask your system administrator where the directory {\tt [isac-bin]} is on your system):
1.67 +\begin{verbatim}
1.68 + > [isac-bin]/sml @SMLload=isac.020120-math
1.69 + val it = false : bool
1.70 + ML>
1.71 +\end{verbatim}
1.72 +yielding the message {\tt val it = false : bool} followed by the prompt of the KE. Having been successful so far, just type in the input presented below -- all of it belongs to {\em one} session~!
1.73 +
1.74 +\chapter{Experimental approach}
1.75 +
1.76 +\section{Basics, terms and parsing}
1.77 +Isabelle implements terms of the {\it simply typed lambda calculus} \cite{typed-lambda} defined in $\sim${\tt/src/Pure.ML}.
1.78 +\subsection{The definition of terms}
1.79 +There are two kinds of terms in Isabelle, 'raw terms' and 'certified terms'. \isac{} works on raw terms, which are efficient but hard to comprehend.
1.80 +{\footnotesize\begin{verbatim}
1.81 + datatype term =
1.82 + Const of string * typ
1.83 + | Free of string * typ
1.84 + | Var of indexname * typ
1.85 + | Bound of int
1.86 + | Abs of string * typ * term
1.87 + | op $ of term * term;
1.88 +
1.89 + datatype typ = Type of string * typ list
1.90 + | TFree of string * sort
1.91 + | TVar of indexname * sort;
1.92 +\end{verbatim}}%size % $
1.93 +where the definitions of sort and indexname is not relevant in this context. The {\tt typ}e is being inferred during parsing. Parsing creates the other kind of terms, {\tt cterm}. These {\tt cterm}s are encapsulated records, which cannot be composed without the respective Isabelle functions (checking for type correctness), but which then are conveniently displayed as strings (using SML compiler internals -- see below).
1.94 +
1.95 +\subsection{Theories and parsing}
1.96 +Parsing uses information contained in Isabelles theories $\sim${\tt /src/HOL}. The currently active theory is held in a global variable {\tt thy}; theories can be accessed individually;
1.97 +{\footnotesize\begin{verbatim}
1.98 + ML> thy;
1.99 + val it =
1.100 + {ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,
1.101 + Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat, Arith,
1.102 + Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype, Numeral, Bin,
1.103 + IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option, Map, Record,
1.104 + RelPow, Sexp, String, Calculation, SVC_Oracle, Main, Zorn, Filter, PNat,
1.105 + PRat, PReal, RealDef, RealOrd, RealInt, RealBin, HyperDef, Descript, ListG,
1.106 + Tools, Script, Typefix, Atools, RatArith, SqRoot, Differentiate, DiffAppl,
1.107 + InsSort, Isac} : theory ML>
1.108 + ML> HOL.thy;
1.109 + val it = {ProtoPure, CPure, HOL} : theory
1.110 + ML>
1.111 + ML> parse;
1.112 + val it = fn : theory -> string -> cterm option
1.113 + ML> parse thy "a + b * #3";
1.114 + val it = Some "a + b * #3" : cterm option
1.115 + ML>
1.116 + ML> val t = (term_of o the) it;
1.117 + val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term
1.118 +\end{verbatim}}%size
1.119 +where {\tt term\_of} and {\tt the} are explained below. The syntax of the list of characters can be read out of Isabelles theories \cite{Isa-obj} {\tt [isabelle]/src/HOL/}\footnote{Or you may use your internetbrowser to look at the files in {\tt [isabelle]/browser\_info}.}
1.120 +and from theories developed with in \isac{} at {\tt [isac-src]/knowledge/}. Note that the syntax of the terms is different from those displayed at \isac's frontend after conversion to MathML.
1.121 +
1.122 +
1.123 +\subsection{Displaying terms}
1.124 +The print depth on the SML top-level can be set in order to produce output in the amount of detail desired:
1.125 +{\footnotesize\begin{verbatim}
1.126 + ML> Compiler.Control.Print.printDepth;
1.127 + val it = ref 4 : int ref
1.128 + ML>
1.129 + ML> Compiler.Control.Print.printDepth:= 2;
1.130 + val it = () : unit
1.131 + ML> t;
1.132 + val it = # $ # $ (# $ #) : term
1.133 + ML>
1.134 + ML> Compiler.Control.Print.printDepth:= 6;
1.135 + val it = () : unit
1.136 + ML> t;
1.137 + val it =
1.138 + Const ("op +","[RealDef.real, RealDef.real] => RealDef.real") $
1.139 + Free ("a","RealDef.real") $
1.140 + (Const ("op *","[RealDef.real, RealDef.real] => RealDef.real") $
1.141 + Free ("b","RealDef.real") $ Free ("#3","RealDef.real")) : term
1.142 +\end{verbatim}}%size % $
1.143 +A closer look to the latter output shows that {\tt typ} is output as a string like {\tt cterm}. Other useful settings for the output are:
1.144 +{\footnotesize\begin{verbatim}
1.145 + ML> Compiler.Control.Print.printLength;
1.146 + val it = ref 8 : int ref
1.147 + ML> Compiler.Control.Print.stringDepth;
1.148 + val it = ref 250 : int ref
1.149 +\end{verbatim}}%size
1.150 +Anyway, the SML output of terms is not very readable; there are functions in the KE to display them:
1.151 +{\footnotesize\begin{verbatim}
1.152 + ML> atomt;
1.153 + val it = fn : term -> unit
1.154 + ML> atomt t;
1.155 + *** -------------
1.156 + *** Const ( op +)
1.157 + *** . Free ( a, )
1.158 + *** . Const ( op *)
1.159 + *** . . Free ( b, )
1.160 + *** . . Free ( #3, )
1.161 + val it = () : unit
1.162 + ML>
1.163 + ML> atomty;
1.164 + val it = fn : theory -> term -> unit
1.165 + ML> atomty thy t;
1.166 + *** -------------
1.167 + *** Const ( op +, [real, real] => real)
1.168 + *** . Free ( a, real)
1.169 + *** . Const ( op *, [real, real] => real)
1.170 + *** . . Free ( b, real)
1.171 + *** . . Free ( #3, real)
1.172 + val it = () : unit
1.173 +\end{verbatim}}%size
1.174 +where again the {\tt typ}s are rendered as strings, but more elegantly by use of the information contained in {\tt thy}..
1.175 +
1.176 +\paragraph{Give it a try !} {\bf The mathematics knowledge grows} as it is defined in Isabelle theory by theory. Have a look by your internet browser to the hierarchy of those theories at {\tt [isabelle]/src/HOL/HOL.thy} and its children available on your system. Or you may use your internetbrowser to look at the files in {\tt [isabelle]/browser\_info}.
1.177 +{\footnotesize\begin{verbatim}
1.178 + ML> (*-1-*) parse HOL.thy "#2^^^#3";
1.179 + *** Inner lexical error at: "^^^#3"
1.180 + val it = None : cterm option
1.181 + ML>
1.182 + ML> (*-2-*) parse HOL.thy "d_d x (a + x)";
1.183 + val it = None : cterm option
1.184 + ML>
1.185 + ML>
1.186 + ML> (*-3-*) parse RatArith.thy "#2^^^#3";
1.187 + val it = Some "#2 ^^^ #3" : cterm option
1.188 + ML>
1.189 + ML> (*-4-*) parse RatArith.thy "d_d x (a + x)";
1.190 + val it = Some "d_d x (a + x)" : cterm option
1.191 + ML>
1.192 + ML>
1.193 + ML> (*-5-*) parse Differentiate.thy "d_d x (a + x)";
1.194 + val it = Some "d_d x (a + x)" : cterm option
1.195 + ML>
1.196 + ML> (*-6-*) parse Differentiate.thy "#2^^^#3";
1.197 + val it = Some "#2 ^^^ #3" : cterm option
1.198 +\end{verbatim}}%size
1.199 +Don't trust the string representation: if we convert {\tt(*-4-*)} and {\tt(*-6-*)} to terms \dots
1.200 +{\footnotesize\begin{verbatim}
1.201 + ML> (*-4-*) val thy = RatArith.thy;
1.202 + ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
1.203 + *** -------------
1.204 + *** Free ( d_d, [real, real] => real)
1.205 + *** . Free ( x, real)
1.206 + *** . Const ( op +, [real, real] => real)
1.207 + *** . . Free ( a, real)
1.208 + *** . . Free ( x, real)
1.209 + val it = () : unit
1.210 + ML>
1.211 + ML> (*-6-*) val thy = Differentiate.thy;
1.212 + ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
1.213 + *** -------------
1.214 + *** Const ( Differentiate.d_d, [real, real] => real)
1.215 + *** . Free ( x, real)
1.216 + *** . Const ( op +, [real, real] => real)
1.217 + *** . . Free ( a, real)
1.218 + *** . . Free ( x, real)
1.219 + val it = () : unit
1.220 +\end{verbatim}}%size
1.221 +\dots we see: in {\tt(*-4-*)} we have an arbitrary function {\tt Free ( d\_d, \_)} and in {\tt(*-6-*)} we have the special function constant {\tt Const ( Differentiate.d\_d, \_)} for differentiation, which is defined in {\tt Differentiate.thy} and presumerably is meant.
1.222 +
1.223 +
1.224 +\subsection{Converting terms}
1.225 +The conversion from {\tt cterm} to {\tt term} has been shown above:
1.226 +{\footnotesize\begin{verbatim}
1.227 + ML> term_of;
1.228 + val it = fn : cterm -> term
1.229 + ML>
1.230 + ML> the;
1.231 + val it = fn : 'a option -> 'a
1.232 + ML>
1.233 + ML> val t = (term_of o the o (parse thy)) "a + b * #3";
1.234 + val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term
1.235 +\end{verbatim}}%size
1.236 +where {\tt the} unwraps the {\tt term option} --- an auxiliary function from Larry Paulsons basic library at {\tt [isabelle]/src/Pure/library.ML}, which is really worthwile to study for any SML programmer.
1.237 +
1.238 +The other conversions are the following, some of which use the {\it signature} {\tt sign} of a theory:
1.239 +{\footnotesize\begin{verbatim}
1.240 + ML> sign_of;
1.241 + val it = fn : theory -> Sign.sg
1.242 + ML>
1.243 + ML> cterm_of;
1.244 + val it = fn : Sign.sg -> term -> cterm
1.245 + ML> val ct = cterm_of (sign_of thy) t;
1.246 + val ct = "a + b * #3" : cterm
1.247 + ML>
1.248 + ML> Sign.string_of_term;
1.249 + val it = fn : Sign.sg -> term -> string
1.250 + ML> Sign.string_of_term (sign_of thy) t;
1.251 + val it = "a + b * #3" : ctem'
1.252 + ML>
1.253 + ML> string_of_cterm;
1.254 + val it = fn : cterm -> string
1.255 + ML> string_of_cterm ct;
1.256 + val it = "a + b * #3" : ctem'
1.257 +\end{verbatim}}%size
1.258 +
1.259 +\subsection{Theorems}
1.260 +Theorems are a type, {\tt thm}, even more protected than {\tt cterms}: they are defined as axioms or proven in Isabelle. These definitions and proofs are contained in theories in the directory {\tt[isac-src]/knowledge/}, e.g. the theorem {\tt diff\_sum} in the theory {\tt[isac-src]/knowledge/Differentiate.thy}. Additionally, each theorem has to be recorded for \isac{} in the respective {\tt *.ML}, e.g. {\tt diff\_sum} in {\tt[isac-src]/knowledge/Differentiate.ML} as follows:
1.261 +{\footnotesize\begin{verbatim}
1.262 + ML> theorem' := overwritel (!theorem',
1.263 + [("diff_const",num_str diff_const)
1.264 + ]);
1.265 +\end{verbatim}}%size
1.266 +The additional recording of theorems and other values will disappear in later versions of \isac.
1.267 +
1.268 +\section{Rewriting}
1.269 +\subsection{The arguments for rewriting}
1.270 +The type identifiers of the arguments and values of the rewrite-functions in \ref{rewrite} differ only in an apostroph: the apostrohped types are re-named strings in order to maintain readability.
1.271 +{\footnotesize\begin{verbatim}
1.272 + ML> HOL.thy;
1.273 + val it = {ProtoPure, CPure, HOL} : theory
1.274 + ML> "HOL.thy" : theory';
1.275 + val it = "HOL.thy" : theory'
1.276 + ML>
1.277 + ML> sqrt_right;
1.278 + val it = fn : rew_ord (* term * term -> bool *)
1.279 + ML> "sqrt_right" : rew_ord';
1.280 + val it = "sqrt_right" : rew_ord'
1.281 + ML>
1.282 + ML> eval_rls;
1.283 + val it =
1.284 + Rls
1.285 + {preconds=[],rew_ord=("sqrt_right",fn),
1.286 + rules=[Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,
1.287 + Thm #,Thm #,Thm #,Thm #,Thm #,Calc #,Calc #,...],
1.288 + scr=Script (Free #)} : rls
1.289 + ML> "eval_rls" : rls';
1.290 + val it = "eval_rls" : rls'
1.291 + ML>
1.292 + ML> diff_sum;
1.293 + val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : thm
1.294 + ML> ("diff_sum", "") : thm';
1.295 + val it = ("diff_sum","") : thm'
1.296 +\end{verbatim}}%size
1.297 +where a {\tt thm'} is a pair, eventually with the string-representation of the respective theorem.
1.298 +
1.299 +\subsection{The functions for rewriting}\label{rewrite}
1.300 +Rewriting comes along with two equivalent functions, where the first is being actually used within the KE, and the second one is useful for tests:
1.301 +{\footnotesize\begin{verbatim}
1.302 + ML> rewrite_;
1.303 + val it = fn
1.304 + : theory
1.305 + -> rew_ord
1.306 + -> rls -> bool -> thm -> term -> (term * term list) option
1.307 + ML>
1.308 + ML> rewrite;
1.309 + val it = fn
1.310 + : theory'
1.311 + -> rew_ord'
1.312 + -> rls' -> bool -> thm' -> cterm' -> (cterm' * cterm' list) option
1.313 +\end{verbatim}}%size
1.314 +The arguments are the following:\\
1.315 +\tabcolsep=4mm
1.316 +\def\arraystretch{1.5}
1.317 +\begin{tabular}{lp{11.0cm}}
1.318 + {\tt theory} & the Isabelle theory containing the definitions necessary for parsing the {\tt term} \\
1.319 + {\tt rew\_ord}& the rewrite order \cite{nipk:rew-all-that} for ordered rewriting -- see the section \ref{term-order} below. For {\em no} ordered rewriting take {\tt tless\_true}, a dummy order yielding true for all arguments \\
1.320 + {\tt rls} & the rule set for evaluating the condition within {\tt thm} in case {\tt thm} is a conditional rule \\
1.321 + {\tt bool} & a flag which triggers the evaluation of the eventual condition in {\tt thm}: if {\tt false} then evaluate the condition and according to the result of the evaluation apply {\tt thm} or not (conditional rewriting \cite{nipk:rew-all-that}), if {\tt true} then don't evaluate the condition, but put it into the set of assumptions \\
1.322 + {\tt thm} & the theorem used to try to rewrite {\tt term} \\
1.323 + {\tt term} & the term eventually rewritten by {\tt thm} \\
1.324 +\end{tabular}\\
1.325 +
1.326 +\noindent The respective values of {\tt rewrite\_} and {\tt rewrite} are an {\tt option} of a pair, i.e. {\tt Some(\_,\_)} in case the {\tt term} can be rewritten by {\tt thm} w.r.t. {\tt rew\_ord} and/or {\tt rls}, or {\tt None} if no rewrite is found:\\
1.327 +\begin{tabular}{lp{10.4cm}}
1.328 + {\tt term} & the term rewritten \\
1.329 + {\tt term list}& the assumptions eventually generated if the {\tt bool} flag is set to {\tt true} and {\tt thm} is applicable. \\
1.330 +\end{tabular}\\
1.331 +
1.332 +\paragraph{Give it a try !} {\bf\dots rewriting is fun~!} many examples can be found in {\tt [isac-src]/tests/\dots}. In {\tt [isac-src]/tests/differentiate.sml} the following can be found:
1.333 +{\footnotesize\begin{verbatim}
1.334 + ML> val thy' = "Differentiate.thy";
1.335 + val thy' = "Differentiate.thy" : string
1.336 + ML> val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
1.337 + val ct = "d_d x (x ^^^ #2 + #3 * x + #4)" : cterm'
1.338 + ML>
1.339 + ML> val thm = ("diff_sum","");
1.340 + val thm = ("diff_sum","") : thm'
1.341 + ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.342 + [("bdv","x::real")] thm ct;
1.343 + val ct = "d_d x (x ^^^ #2 + #3 * x) + d_d x #4" : cterm'
1.344 + ML>
1.345 + ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.346 + [("bdv","x::real")] thm ct;
1.347 + val ct = "d_d x (x ^^^ #2) + d_d x (#3 * x) + d_d x #4" : cterm'
1.348 + ML>
1.349 + ML> val thm = ("diff_prod_const","");
1.350 + val thm = ("diff_prod_const","") : thm'
1.351 + ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.352 + [("bdv","x::real")] thm ct;
1.353 + val ct = "d_d x (x ^^^ #2) + #3 * d_d x x + d_d x #4" : cterm'
1.354 +\end{verbatim}}%size
1.355 +You can look up the theorems in {\tt [isac-src]/knowledge/Differentiate.thy} and try to apply them until you get the result you would expect if calculating by hand.
1.356 +\footnote{Hint: At the end you will need {\tt val (ct,\_) = the (rewrite\_set thy' "eval\_rls" false "SqRoot\_simplify" ct);}}
1.357 +
1.358 +\paragraph{Give it a try !}\label{cond-rew} {\bf Conditional rewriting} is a more powerful technique then ordinary rewriting, and is closer to the power of programming languages (see the subsequent 'try it out'~!). The following example expands a term to poynomial form:
1.359 +{\footnotesize\begin{verbatim}
1.360 + ML> val thy' = "Isac.thy";
1.361 + val thy' = "Isac.thy" : string
1.362 + ML> val ct' = "#3 * a + #2 * (a + #1)";
1.363 + val ct' = "#3 * a + #2 * (a + #1)" : cterm'
1.364 + ML>
1.365 + ML> val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");
1.366 + val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n")
1.367 + : thm'
1.368 + ML> (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.369 + val ct' = "#3 * a + (#2 * a + #2 * #1)" : cterm'
1.370 + ML>
1.371 + ML> val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");
1.372 + val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1")
1.373 + : thm'
1.374 + ML> (*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.375 + val ct' = "#3 * a + #2 * a + #2 * #1" : cterm'
1.376 + ML>
1.377 + ML> val thm' = ("rcollect_right",
1.378 + "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");
1.379 + val thm' =
1.380 + ("rcollect_right",
1.381 + "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n")
1.382 + : thm'
1.383 + ML> (*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.384 + val ct' = "(#3 + #2) * a + #2 * #1" : cterm'
1.385 + ML>
1.386 + ML> (*4*) val Some (ct',_) = calculate' thy' "plus" ct';
1.387 + val ct' = "#5 * a + #2 * #1" : cterm'
1.388 + ML>
1.389 + ML> (*5*) val Some (ct',_) = calculate' thy' "times" ct';
1.390 + val ct' = "#5 * a + #2" : cterm'
1.391 +\end{verbatim}}%size
1.392 +Note, that the two rules, {\tt radd\_mult\_distrib2} in {\tt(*1*)} and {\tt rcollect\_right} in {\tt(*3*)} would neutralize each other (i.e. a rule set would not terminate), if there would not be the condition {\tt is\_const}.
1.393 +
1.394 +\paragraph{Give it a try !} {\bf Functional programming} can, within a certain range, modeled by rewriting. In {\tt [isac-src]/\dots/tests/InsSort.thy} the following rules can be found, which are able to sort a list ('insertion sort'):
1.395 +{\footnotesize\begin{verbatim}
1.396 + sort_def "sort ls = foldr ins ls []"
1.397 +
1.398 + ins_base "ins [] a = [a]"
1.399 + ins_rec "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))"
1.400 +
1.401 + foldr_base "foldr f [] a = a"
1.402 + foldr_rec "foldr f (x#xs) a = foldr f xs (f a x)"
1.403 +
1.404 + if_True "(if True then ?x else ?y) = ?x"
1.405 + if_False "(if False then ?x else ?y) = ?y"
1.406 +\end{verbatim}}%size
1.407 +where {\tt\#} is the list-constructor, {\tt foldr} is the well-known standard function of functional programming, and {\tt if\_True, if\_False} are auxiliary rules. Then the sort may be done by the following rewrites:
1.408 +{\footnotesize\begin{verbatim}
1.409 + ML> val thy' = "InsSort.thy";
1.410 + val thy' = "InsSort.thy" : theory'
1.411 + ML> val ct = "sort [#1,#3,#2]" : cterm';
1.412 + val ct = "sort [#1,#3,#2]" : cterm'
1.413 + ML>
1.414 + ML> val thm = ("sort_def","");
1.415 + ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.416 + val ct = "foldr ins [#1, #3, #2] []" : cterm'
1.417 + ML>
1.418 + ML> val thm = ("foldr_rec","");
1.419 + ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.420 + val ct = "foldr ins [#3, #2] (ins [] #1)" : cterm'
1.421 + ML>
1.422 + ML> val thm = ("ins_base","");
1.423 + ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.424 + val ct = "foldr ins [#3, #2] [#1]" : cterm'
1.425 + ML>
1.426 + ML> val thm = ("foldr_rec","");
1.427 + ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.428 + val ct = "foldr ins [#2] (ins [#1] #3)" : cterm'
1.429 + ML>
1.430 + ML> val thm = ("ins_rec","");
1.431 + ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.432 + val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"
1.433 + : cterm'
1.434 + ML>
1.435 + ML> val (ct,_) = the (calculate' thy' "le" ct);
1.436 + val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])" : cterm'
1.437 + ML>
1.438 + ML> val thm = ("if_True","(if True then ?x else ?y) = ?x");
1.439 + ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.440 + val ct = "foldr ins [#2] (#1 # ins [] #3)" : cterm'
1.441 + ML>
1.442 + ...
1.443 + val ct = "sort [#1,#3,#2]" : cterm'
1.444 +\end{verbatim}}%size
1.445 +
1.446 +
1.447 +\subsection{Variants of rewriting}
1.448 +Some of the above examples already used variants of {\tt rewrite} all of which have the same value, and very similar arguments:
1.449 +{\footnotesize\begin{verbatim}
1.450 + ML> rewrite_inst_;
1.451 + val it = fn
1.452 + : theory
1.453 + -> rew_ord
1.454 + -> rls
1.455 + -> bool
1.456 + -> (cterm' * cterm') list
1.457 + -> thm -> term -> (term * term list) option
1.458 + ML> rewrite_inst;
1.459 + val it = fn
1.460 + : theory'
1.461 + -> rew_ord'
1.462 + -> rls'
1.463 + -> bool
1.464 + -> (cterm' * cterm') list
1.465 + -> thm' -> cterm' -> (cterm' * cterm' list) option
1.466 + ML>
1.467 + ML> rewrite_set_;
1.468 + val it = fn
1.469 + : theory -> rls -> bool -> rls -> term -> (term * term list) option
1.470 + ML> rewrite_set;
1.471 + val it = fn
1.472 + : theory' -> rls' -> bool -> rls' -> cterm' -> (cterm' * cterm' list) option
1.473 + ML>
1.474 + ML> rewrite_set_inst_;
1.475 + val it = fn
1.476 + : theory
1.477 + -> rls
1.478 + -> bool
1.479 + -> (cterm' * cterm') list
1.480 + -> rls -> term -> (term * term list) option
1.481 + ML> rewrite_set_inst;
1.482 + val it = fn
1.483 + : theory'
1.484 + -> rls'
1.485 + -> bool
1.486 + -> (cterm' * cterm') list
1.487 + -> rls' -> cterm' -> (cterm' * cterm' list) option
1.488 +\end{verbatim}}%size
1.489 +
1.490 +\noindent The variant {\tt rewrite\_inst} substitutes {\tt (term * term) list} in {\tt thm} before rewriting,\\
1.491 +the variant {\tt rewrite\_set} rewrites with a whole rule set {\tt rls} (instead with a {\tt thm} only),\\
1.492 +the variant {\tt rewrite\_set\_inst} is a combination of the latter two variants. In order to watch how a term is rewritten theorem by theorem, there is a switch {\tt trace\_rewrite}:
1.493 +{\footnotesize\begin{verbatim}
1.494 + ML> toggle;
1.495 + val it = fn : bool ref -> bool
1.496 + ML>
1.497 + ML> toggle trace_rewrite;
1.498 + val it = true : bool
1.499 + ML> toggle trace_rewrite;
1.500 + val it = false : bool
1.501 +\end{verbatim}}%size
1.502 +
1.503 +\subsection{Rule sets}
1.504 +Some of the variants of {\tt rewrite} above do not only apply one theorem, but a whole set of theorems, called a 'rule set'. Such a rule set is applied as long one of its elements can be used for a rewrite (which can go forever, i.e. the rule set eventually does not 'terminate').
1.505 +
1.506 +A simple example of a rule set is {\tt rearrange\_assoc} which is defined in {\tt knowledge/RatArith.ML} as:
1.507 +{\footnotesize\begin{verbatim}
1.508 + val rearrange_assoc =
1.509 + Rls{preconds = [], rew_ord = ("tless_true",tless_true),
1.510 + rules =
1.511 + [Thm ("radd_assoc_RS_sym",num_str (radd_assoc RS sym)),
1.512 + Thm ("rmult_assoc_RS_sym",num_str (rmult_assoc RS sym))],
1.513 + scr = Script ((term_of o the o (parse thy))
1.514 + "empty_script")
1.515 + }:rls;
1.516 +\end{verbatim}}%size
1.517 +where
1.518 +\begin{description}
1.519 +\item [\tt preconds] are conditions which must be true in order to make the rule set applicable (the empty list evaluates to {\tt true})
1.520 +\item [\tt rew\_ord] concerns term orders introduced below in \ref{term-order}
1.521 +\item [\tt rules] are the theorems to be applied -- in priciple applied in arbitrary order, because all these rule sets should be 'complete' \cite{nipk:rew-all-that} (and actually the theorems are applied in the sequence they appear in this list). The function {\tt num\_str} must be applied to theorems containing numeral constants (and thus is obsolete in this example). {\tt RS} is an infix function applying the theorem {\tt sym} to {\tt radd\_assoc} before storage (the effect see below)
1.522 +\item [\tt scr] is the script applying the ruleset; it will disappear in later versions of \isac.
1.523 +\end{description}
1.524 +These variables evaluate to
1.525 +{\footnotesize\begin{verbatim}
1.526 + ML> sym;
1.527 + val it = "?s = ?t ==> ?t = ?s" : thm
1.528 + ML> rearrange_assoc;
1.529 + val it =
1.530 + Rls
1.531 + {preconds=[],rew_ord=("tless_true",fn),
1.532 + rules=[Thm ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"),
1.533 + Thm ("rmult_assoc_RS_sym","?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")],
1.534 + scr=Script (Free ("empty_script","RealDef.real"))} : rls
1.535 +\end{verbatim}}%size
1.536 +
1.537 +\paragraph{Give it a try !} The above rule set makes an arbitrary number of parentheses disappear which are not necessary due to associativity of {\tt +} and
1.538 +{\footnotesize\begin{verbatim}
1.539 + ML> val ct = (string_of_cterm o the o (parse RatArith.thy))
1.540 + "a + (b * (c * d) + e)";
1.541 + val ct = "a + ((b * (c * d) + e) + f)" : cterm'
1.542 + ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
1.543 + val it = Some ("a + b * c * d + e + f",[]) : (string * string list) option
1.544 +\end{verbatim}}%size
1.545 +For acchieving this result the rule set has to be surprisingly busy:
1.546 +{\footnotesize\begin{verbatim}
1.547 + ML> toggle trace_rewrite;
1.548 + val it = true : bool
1.549 + ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
1.550 + ### trying thm 'radd_assoc_RS_sym'
1.551 + ### rewrite_set_: a + b * (c * d) + e
1.552 + ### trying thm 'radd_assoc_RS_sym'
1.553 + ### trying thm 'rmult_assoc_RS_sym'
1.554 + ### rewrite_set_: a + b * c * d + e
1.555 + ### trying thm 'rmult_assoc_RS_sym'
1.556 + ### trying thm 'radd_assoc_RS_sym'
1.557 + ### trying thm 'rmult_assoc_RS_sym'
1.558 + val it = Some ("a + b * c * d + e",[]) : (string * string list) option
1.559 +\end{verbatim}}%size
1.560 +
1.561 +
1.562 +\subsection{Calculate numeric constants}
1.563 +As soon as numeric constants are in adjacent subterms (see the example on p.\pageref{cond-rew}), they can be calculated by the function
1.564 +{\footnotesize\begin{verbatim}
1.565 + ML> calculate;
1.566 + val it = fn : theory' -> string -> cterm' -> (cterm' * thm') option
1.567 + ML> calculate_;
1.568 + val it = fn : theory -> string -> term -> (term * (string * thm)) option
1.569 +\end{verbatim}}%size
1.570 +where the {\tt string} in the arguments defines the algebraic operation to be calculated. The function returns the result of the calculation, and as second element in the pair the theorem applied. The following algebraic operations are available:
1.571 +{\footnotesize\begin{verbatim}
1.572 + ML> calc_list;
1.573 + val it =
1.574 + ref
1.575 + [("plus",("op +",fn)),
1.576 + ("times",("op *",fn)),
1.577 + ("cancel_",("cancel",fn)),
1.578 + ("power",("pow",fn)),
1.579 + ("sqrt",("sqrt",fn)),
1.580 + ("Var",("Var",fn)),
1.581 + ("Length",("Length",fn)),
1.582 + ("Nth",("Nth",fn)),
1.583 + ("power",("pow",fn)),
1.584 + ("le",("op <",fn)),
1.585 + ("leq",("op <=",fn)),
1.586 + ("is_const",("is'_const",fn)),
1.587 + ("is_root_free",("is'_root'_free",fn)),
1.588 + ("contains_root",("contains'_root",fn)),
1.589 + ("ident",("ident",fn))]
1.590 + : (string * (string * (string -> term -> theory ->
1.591 + (string * term) option))) list ref
1.592 +\end{verbatim}}%size
1.593 +These operations can be used in the following way.
1.594 +{\footnotesize\begin{verbatim}
1.595 + ML> calculate' "Isac.thy" "plus" "#1 + #2";
1.596 + val it = Some ("#3",("#add_#1_#2","\"#1 + #2 = #3\"")) : (string * thm') option
1.597 + ML>
1.598 + ML> calculate' "Isac.thy" "times" "#2 * #3";
1.599 + val it = Some ("#6",("#mult_#2_#3","\"#2 * #3 = #6\""))
1.600 + : (string * thm') option
1.601 + ML>
1.602 + ML> calculate' "Isac.thy" "power" "#2 ^^^ #3";
1.603 + val it = Some ("#8",("#power_#2_#3","\"#2 ^^^ #3 = #8\""))
1.604 + : (string * thm') option
1.605 + ML>
1.606 + ML> calculate' "Isac.thy" "cancel_" "#9 // #12";
1.607 + val it = Some ("#3 // #4",("#cancel_#9_#12","\"#9 // #12 = #3 // #4\""))
1.608 + : (string * thm') option
1.609 + ML>
1.610 + ML> ...
1.611 +\end{verbatim}}%size
1.612 +
1.613 +
1.614 +
1.615 +\section{Term orders}\label{term-order}
1.616 +Orders on terms are indispensable for the purpose of rewriting to normal forms in associative - commutative domains \cite{nipk:rew-all-that}, and for rewriting to normal forms necessary for matching models to problems, see sect.\ref{pbt}.
1.617 +\subsection{Examples for term orders}
1.618 +It is not trivial to construct a relation $<$ on terms such that it is really an order, i.e. a transitive and antisymmetric relation. These orders are 'recursive path orders' \cite{nipk:rew-all-that}. Some orders implemented in the knowledgebase at {\tt [isac-src]/knowledge/\dots}, %FIXXXmat0201a
1.619 +e.g.
1.620 +{\footnotesize\begin{verbatim}
1.621 + ML> sqrt_right;
1.622 + val it = fn : bool -> theory -> term * term -> bool
1.623 + ML> tless_true;
1.624 + val it = fn : 'a -> bool
1.625 +\end{verbatim}}%size
1.626 +where the bool argument is a switch for tracing the checks on the respective subterms (and theory is necessary for displyinging the (sub-)terms as strings in the case of 'true'). The order {\tt tless\_true} is a dummy always yielding {\tt true}, and {\tt sqrt\_right} prefers a square root shifted to the right within a term:
1.627 +{\footnotesize\begin{verbatim}
1.628 + ML> val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";
1.629 + val t1 = Const # $ (# $ #) $ Free (#,#) : term
1.630 + ML>
1.631 + ML> val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";
1.632 + val t2 = Const # $ Free # $ (Const # $ Free #) : term
1.633 + ML>
1.634 + ML> sqrt_right false SqRoot.thy (t1, t2);
1.635 + val it = false : bool
1.636 + ML> sqrt_right false SqRoot.thy (t2, t1);
1.637 + val it = true : bool
1.638 +\end{verbatim}}%size
1.639 +The many checks performed recursively through all subterms can be traced throughout the algorithm in {\tt [isac-src]/knowledge/SqRoot.ML} by setting the flag to true:
1.640 +{\footnotesize\begin{verbatim}
1.641 + ML> val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";
1.642 + val t1 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term
1.643 + ML>
1.644 + ML> val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";
1.645 + val t2 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term
1.646 + ML>
1.647 + ML> sqrt_right true SqRoot.thy (t1, t2);
1.648 + t= f@ts= "op +" @ "[a + b * sqrt c,d]"
1.649 + u= g@us= "op +" @ "[a + sqrt b * c,d]"
1.650 + size_of_term(t,u)= (8, 8)
1.651 + hd_ord(f,g) = EQUAL
1.652 + terms_ord(ts,us) = LESS
1.653 + -------
1.654 + t= f@ts= "op +" @ "[a,b * sqrt c]"
1.655 + u= g@us= "op +" @ "[a,sqrt b * c]"
1.656 + size_of_term(t,u)= (6, 6)
1.657 + hd_ord(f,g) = EQUAL
1.658 + terms_ord(ts,us) = LESS
1.659 + -------
1.660 + t= f@ts= "a" @ "[]"
1.661 + u= g@us= "a" @ "[]"
1.662 + size_of_term(t,u)= (1, 1)
1.663 + hd_ord(f,g) = EQUAL
1.664 + terms_ord(ts,us) = EQUAL
1.665 + -------
1.666 + t= f@ts= "op *" @ "[b,sqrt c]"
1.667 + u= g@us= "op *" @ "[sqrt b,c]"
1.668 + size_of_term(t,u)= (4, 4)
1.669 + hd_ord(f,g) = EQUAL
1.670 + terms_ord(ts,us) = LESS
1.671 + -------
1.672 + t= f@ts= "b" @ "[]"
1.673 + u= g@us= "sqrt" @ "[b]"
1.674 + size_of_term(t,u)= (1, 2)
1.675 + hd_ord(f,g) = LESS
1.676 + terms_ord(ts,us) = LESS
1.677 + -------
1.678 + val it = true : bool
1.679 +\end{verbatim}}%size
1.680 +
1.681 +
1.682 +
1.683 +\subsection{Ordered rewriting}
1.684 +Rewriting faces problems in just the most elementary domains, which are all associative and commutative w.r.t. {\tt +} and {\tt *} --- the law of commutativity applied within a rule set causes this set not to terminate~! One method to cope with this difficulty is ordered rewriting, where a rewrite is only done if the resulting term is smaller w.r.t. a term order (with some additional properties called 'rewrite orders' \cite{nipk:rew-all-that}).
1.685 +
1.686 +Such a rule set {\tt ac\_plus\_times}, called an AC-rewrite system, can be found in {\tt[isac-src]/knowledge/RathArith.ML}:
1.687 +{\footnotesize\begin{verbatim}
1.688 + val ac_plus_times =
1.689 + Rls{preconds = [], rew_ord = ("term_order",term_order),
1.690 + rules =
1.691 + [Thm ("radd_commute",radd_commute),
1.692 + Thm ("radd_left_commute",radd_left_commute),
1.693 + Thm ("radd_assoc",radd_assoc),
1.694 + Thm ("rmult_commute",rmult_commute),
1.695 + Thm ("rmult_left_commute",rmult_left_commute),
1.696 + Thm ("rmult_assoc",rmult_assoc)],
1.697 + scr = Script ((term_of o the o (parse thy))
1.698 + "empty_script")
1.699 + }:rls;
1.700 + val ac_plus_times =
1.701 + Rls
1.702 + {preconds=[],rew_ord=("term_order",fn),
1.703 + rules=[Thm ("radd_commute","?m + ?n = ?n + ?m"),
1.704 + Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"),
1.705 + Thm ("radd_assoc","?m + ?n + ?k = ?m + (?n + ?k)"),
1.706 + Thm ("rmult_commute","?m * ?n = ?n * ?m"),
1.707 + Thm ("rmult_left_commute","?x * (?y * ?z) = ?y * (?x * ?z)"),
1.708 + Thm ("rmult_assoc","?m * ?n * ?k = ?m * (?n * ?k)")],
1.709 + scr=Script (Free ("empty_script","RealDef.real"))} : rls
1.710 +\end{verbatim}}%size
1.711 +Note that the theorems {\tt radd\_left\_commute} and {\tt rmult\_left\_commute} are really necessary in order to make the rule set 'confluent'~!
1.712 +
1.713 +
1.714 +\paragraph{Give it a try !} Ordered rewriting is one technique to produce polynomial normal from from arbitrary integer terms:
1.715 +{\footnotesize\begin{verbatim}
1.716 + ML> val ct' = "#3 * a + b + #2 * a";
1.717 + val ct' = "#3 * a + b + #2 * a" : cterm'
1.718 + ML>
1.719 + ML> (*-1-*) radd_commute; val thm' = ("radd_commute","") : thm';
1.720 + val it = "?m + ?n = ?n + ?m" : thm
1.721 + val thm' = ("radd_commute","") : thm'
1.722 + ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.723 + val ct' = "#2 * a + (#3 * a + b)" : cterm'
1.724 + ML>
1.725 + ML> (*-2-*) rdistr_right_assoc_p; val thm' = ("rdistr_right_assoc_p","") : thm';
1.726 + val it = "?l * ?n + (?m * ?n + ?k) = (?l + ?m) * ?n + ?k" : thm
1.727 + val thm' = ("rdistr_right_assoc_p","") : thm'
1.728 + ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.729 + val ct' = "(#2 + #3) * a + b" : cterm'
1.730 + ML>
1.731 + ML> (*-3-*)
1.732 + ML> val Some (ct',_) = calculate thy' "plus" ct';
1.733 + val ct' = "#5 * a + b" : cterm'
1.734 +\end{verbatim}}%size %FIXXXmat0201b ... calculate !
1.735 +This looks nice, but if {\tt radd\_commute} is applied automatically in {\tt (*-1-*)} without checking the resulting term to be 'smaller' w.r.t. a term order, then rewritin goes on forever (i.e. it does not 'terminate') \dots
1.736 +{\footnotesize\begin{verbatim}
1.737 + ML> val ct' = "#3 * a + b + #2 * a" : cterm';
1.738 + val ct' = "#3 * a + b + #2 * a" : cterm'
1.739 + ML> val thm' = ("radd_commute","") : thm';
1.740 + val thm' = ("radd_commute","") : thm'
1.741 + ML>
1.742 + ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.743 + val ct' = "#2 * a + (#3 * a + b)" : cterm'
1.744 + ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.745 + val ct' = "#3 * a + b + #2 * a" : cterm'
1.746 + ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.747 + val ct' = "#2 * a + (#3 * a + b)" : cterm'
1.748 + ..........
1.749 +\end{verbatim}}%size
1.750 +
1.751 +Ordered rewriting with the above AC-rewrite system {\tt ac\_plus\_times} performs a kind of bubble sort which can be traced:
1.752 +{\footnotesize\begin{verbatim}
1.753 + ML> toggle trace_rewrite;
1.754 + val it = true : bool
1.755 + ML>
1.756 + ML> rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;
1.757 + ### trying thm 'radd_commute'
1.758 + ### not: "a + (b * (c * d) + e)" > "b * (c * d) + e + a"
1.759 + ### rewrite_set_: a + (e + b * (c * d))
1.760 + ### trying thm 'radd_commute'
1.761 + ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"
1.762 + ### not: "e + b * (c * d)" > "b * (c * d) + e"
1.763 + ### trying thm 'radd_left_commute'
1.764 + ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"
1.765 + ### trying thm 'radd_assoc'
1.766 + ### trying thm 'rmult_commute'
1.767 + ### not: "b * (c * d)" > "c * d * b"
1.768 + ### not: "c * d" > "d * c"
1.769 + ### trying thm 'rmult_left_commute'
1.770 + ### not: "b * (c * d)" > "c * (b * d)"
1.771 + ### trying thm 'rmult_assoc'
1.772 + ### trying thm 'radd_commute'
1.773 + ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"
1.774 + ### not: "e + b * (c * d)" > "b * (c * d) + e"
1.775 + ### trying thm 'radd_left_commute'
1.776 + ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"
1.777 + ### trying thm 'radd_assoc'
1.778 + ### trying thm 'rmult_commute'
1.779 + ### not: "b * (c * d)" > "c * d * b"
1.780 + ### not: "c * d" > "d * c"
1.781 + ### trying thm 'rmult_left_commute'
1.782 + ### not: "b * (c * d)" > "c * (b * d)"
1.783 + ### trying thm 'rmult_assoc'
1.784 + val it = Some ("a + (e + b * (c * d))",[]) : (string * string list) option \end{verbatim}}%size
1.785 +Notice that {\tt +} is left-associative where the parentheses are omitted for {\tt (a + b) + c = a + b + c}, but not for {\tt a + (b + c)}. Ordered rewriting necessarily terminates with parentheses which could be omitted due to associativity.
1.786 +
1.787 +
1.788 +\section{The hierarchy of problem types}\label{pbt}
1.789 +\subsection{The standard-function for 'matching'}
1.790 +Matching \cite{nipk:rew-all-that} is a technique used within rewriting, and used by \isac{} also for (a generalized) 'matching' a problem with a problem type. The function which tests for matching has the following signature:
1.791 +{\footnotesize\begin{verbatim}
1.792 + ML> matches;
1.793 + val it = fn : theory -> term -> term -> bool
1.794 +\end{verbatim}}%size
1.795 +where the first of the two {\tt term} arguments is the particular term to be tested, and the second one is the pattern:
1.796 +{\footnotesize\begin{verbatim}
1.797 + ML> val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1";
1.798 + val t = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#1","RealDef.real") : term
1.799 + ML>
1.800 + ML> val p = (term_of o the o (parse thy)) "a * b^^^#2 = c";
1.801 + val p = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("c","RealDef.real") : term
1.802 + ML> atomt p;
1.803 + *** -------------
1.804 + *** Const ( op =)
1.805 + *** . Const ( op *)
1.806 + *** . . Free ( a, )
1.807 + *** . . Const ( RatArith.pow)
1.808 + *** . . . Free ( b, )
1.809 + *** . . . Free ( #2, )
1.810 + *** . Free ( c, )
1.811 + val it = () : unit
1.812 + ML>
1.813 + ML> free2var;
1.814 + val it = fn : term -> term
1.815 + ML>
1.816 + ML> val pat = free2var p;
1.817 + val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term
1.818 + ML> Sign.string_of_term (sign_of thy) pat;
1.819 + val it = "?a * ?b ^^^ #2 = ?c" : cterm'
1.820 + ML> atomt pat;
1.821 + *** -------------
1.822 + *** Const ( op =)
1.823 + *** . Const ( op *)
1.824 + *** . . Var ((a, 0), )
1.825 + *** . . Const ( RatArith.pow)
1.826 + *** . . . Var ((b, 0), )
1.827 + *** . . . Free ( #2, )
1.828 + *** . Var ((c, 0), )
1.829 + val it = () : unit
1.830 +\end{verbatim}}%size % $
1.831 +Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt free2var}. This format of the pattern is necessary in order to obtain results like these:
1.832 +{\footnotesize\begin{verbatim}
1.833 + ML> matches thy t pat;
1.834 + val it = true : bool
1.835 + ML>
1.836 + ML> val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1";
1.837 + val t2 = Const (#,#) $ (# $ # $ Free #) $ Free ("#1","RealDef.real") : term
1.838 + ML> matches thy t2 pat;
1.839 + val it = false : bool
1.840 + ML>
1.841 + ML> val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v";
1.842 + val pat2 = Const (#,#) $ (# $ # $ Free #) $ Var ((#,#),"RealDef.real") : term
1.843 + ML> matches thy t2 pat2;
1.844 + val it = true : bool
1.845 +\end{verbatim}}%size % $
1.846 +
1.847 +\subsection{Accessing the hierarchy}
1.848 +The hierarchy of problem types is encapsulated; it can be accessed by the following functions. {\tt show\_ptyps} retrieves all leaves of the hierarchy (here in an early version for testing):
1.849 +{\footnotesize\begin{verbatim}
1.850 + ML> show_ptyps;
1.851 + val it = fn : unit -> unit
1.852 + ML> show_ptyps();
1.853 + [
1.854 + ["e_pblID"],
1.855 + ["equation", "univariate", "linear"],
1.856 + ["equation", "univariate", "plain_square"],
1.857 + ["equation", "univariate", "polynomial", "degree_two", "pq_formula"],
1.858 + ["equation", "univariate", "polynomial", "degree_two", "abc_formula"],
1.859 + ["equation", "univariate", "squareroot"],
1.860 + ["equation", "univariate", "normalize"],
1.861 + ["equation", "univariate", "sqroot-test"],
1.862 + ["function", "derivative_of"],
1.863 + ["function", "maximum_of", "on_interval"],
1.864 + ["function", "make"],
1.865 + ["tool", "find_values"],
1.866 + ["functional", "inssort"]
1.867 + ]
1.868 + val it = () : unit
1.869 +\end{verbatim}}%size
1.870 +The retrieve function for individual problem types is {\tt get\_pbt}
1.871 +\footnote{A function providing better readable output is in preparation}. Note that its argument, the 'problem identifier' {\tt pblID}, has the strings listed in reverse order w.r.t. the hierarchy, i.e. from the leave to the root. This order makes the {\tt pblID} closer to a natural description:
1.872 +{\footnotesize\begin{verbatim}
1.873 + ML> get_pbt;
1.874 + val it = fn : pblID -> pbt
1.875 + ML> get_pbt ["squareroot", "univariate", "equation"];
1.876 + val it =
1.877 + {met=[("SqRoot.thy","square_equation")],
1.878 + ppc=[("#Given",(Const (#,#),Free (#,#))),
1.879 + ("#Given",(Const (#,#),Free (#,#))),
1.880 + ("#Given",(Const (#,#),Free (#,#))),
1.881 + ("#Find",(Const (#,#),Free (#,#)))],
1.882 + thy={ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,
1.883 + Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat,
1.884 + Arith, Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype,
1.885 + Numeral, Bin, IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option,
1.886 + Map, Record, RelPow, Sexp, String, Calculation, SVC_Oracle, Main,
1.887 + Zorn, Filter, PNat, PRat, PReal, RealDef, RealOrd, RealInt, RealBin,
1.888 + HyperDef, Descript, ListG, Tools, Script, Typefix, Atools, RatArith,
1.889 + SqRoot},
1.890 + where_=[Const ("SqRoot.contains'_root","bool => bool") $
1.891 + Free ("e_","bool")]} : pbt
1.892 +\end{verbatim}}%size %$
1.893 +where the records fields hold the following data:
1.894 +\begin{description}
1.895 +\item [\tt thy]: the theory necessary for parsing the formulas
1.896 +\item [\tt ppc]: the items of the problem type, divided into those {\tt Given}, the precondition {\tt Where} and the output item(s) {\tt Find}. The items of {\tt Given} and {\tt Find} are all headed by so-called descriptions, which determine the type. These descriptions are defined in {\tt [isac-src]/Isa99/Descript.thy}.
1.897 +\item [\tt met]: the list of methods solving this problem type.\\
1.898 +\end{description}
1.899 +
1.900 +The following function adds or replaces a problem type (after having it prepared using {\tt prep\_pbt})
1.901 +{\footnotesize\begin{verbatim}
1.902 + ML> store_pbt;
1.903 + val it = fn : pbt * pblID -> unit
1.904 + ML> store_pbt
1.905 + (prep_pbt SqRoot.thy
1.906 + (["newtype","univariate","equation"],
1.907 + [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
1.908 + ("#Where" ,["contains_root (e_::bool)"]),
1.909 + ("#Find" ,["solutions v_i_"])
1.910 + ],
1.911 + [("SqRoot.thy","square_equation")]));
1.912 + val it = () : unit
1.913 +\end{verbatim}}%size
1.914 +When adding a new type with argument {\tt pblID}, an immediate parent must already exist in the hierarchy (this is the one with the tail of {\tt pblID}).
1.915 +
1.916 +\subsection{Internals of the datastructure}
1.917 +This subsection only serves for the implementation of the hierarchy browser and can be skipped by the authors of math knowledge.
1.918 +
1.919 +A problem type is described by the following record type (in the file {\tt [isac-src]/globals.sml}, the respective functions are in {\tt [isac-src]/ME/ptyps.sml}), and held in a global reference variable:
1.920 +{\footnotesize\begin{verbatim}
1.921 + type pbt =
1.922 + {thy : theory, (* the nearest to the root,
1.923 + which allows to compile that pbt *)
1.924 + where_: term list, (* where - predicates *)
1.925 + ppc : ((string * (* fields "#Given","#Find" *)
1.926 + (term * (* description *)
1.927 + term)) (* id *)
1.928 + list),
1.929 + met : metID list}; (* methods solving the pbt *)
1.930 + datatype ptyp =
1.931 + Ptyp of string * (* key within pblID *)
1.932 + pbt list * (* several pbts with different domIDs*)
1.933 + ptyp list;
1.934 + val e_Ptyp = Ptyp ("empty",[],[]);
1.935 +
1.936 + type ptyps = ptyp list;
1.937 + val ptyps = ref ([e_Ptyp]:ptyps);
1.938 +\end{verbatim}}%size
1.939 +The predicates in {\tt where\_} (i.e. the preconditions) usually are defined in the respective theory in {\tt[isac-src]/knowledge}. Most of the predicates are not defined by rewriting, but by SML-code contained in the respective {\tt *.ML} file.
1.940 +
1.941 +Each item is headed by a so-called description which provides some guidance for interactive input. The descriptions are defined in {\tt[isac-src]/Isa99/Descript.thy}.
1.942 +
1.943 +
1.944 +
1.945 +\subsection{Match a formalization with a problem type}\label{pbl}
1.946 +A formalization is {\it match}ed with a problem type which yields a problem. A formal description of this kind of {\it match}ing can be found in \\{\tt ftp://ft.ist.tugraz.at/projects/isac/publ/calculemus01.ps.gz}. A formalization of an equation is e.g.
1.947 +{\footnotesize\begin{verbatim}
1.948 + ML> val fmz = ["equality (#1 + #2 * x = #0)",
1.949 + "solveFor x",
1.950 + "solutions L"] : fmz;
1.951 + val fmz = ["equality (#1 + #2 * x = #0)","solveFor x","solutions L"] : fmz
1.952 +\end{verbatim}}%size
1.953 +Given a formalization (and a specification of the problem, i.e. a theory, a problemtype, and a method) \isac{} can solve the respective problem automatically. The formalization must match the problem type for this purpose:
1.954 +{\footnotesize\begin{verbatim}
1.955 + ML> match_pbl;
1.956 + val it = fn : fmz -> pbt -> match'
1.957 + ML>
1.958 + ML> match_pbl fmz (get_pbt ["univariate","equation"]);
1.959 + val it =
1.960 + Matches'
1.961 + {Find=[Correct "solutions L"],
1.962 + Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
1.963 + Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]}
1.964 + : match'
1.965 + ML>
1.966 + ML> match_pbl fmz (get_pbt ["linear","univariate","equation"]);
1.967 + val it =
1.968 + Matches'
1.969 + {Find=[Correct "solutions L"],
1.970 + Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
1.971 + Relate=[],
1.972 + Where=[Correct
1.973 + "matches ( x = #0) (#1 + #2 * x = #0) |
1.974 + matches ( ?b * x = #0) (#1 + #2 * x = #0) |
1.975 + matches (?a + x = #0) (#1 + #2 * x = #0) |
1.976 + matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"],
1.977 + With=[]} : match'
1.978 + ML>
1.979 + ML> match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);
1.980 + val it =
1.981 + NoMatch'
1.982 + {Find=[Correct "solutions L"],
1.983 + Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x",
1.984 + Missing "errorBound err_"],Relate=[],
1.985 + Where=[False "contains_root #1 + #2 * x = #0 "],With=[]} : match'
1.986 +\end{verbatim}}%size
1.987 +The above formalization does not match the problem type \\{\tt["squareroot","univariate","equation"]} which is explained by the tags:
1.988 +\begin{tabbing}
1.989 +123\=\kill
1.990 +\> {\tt Missing:} the item is missing in the formalization as required by the problem type\\
1.991 +\> {\tt Superfl:} the item is not required by the problem type\\
1.992 +\> {\tt Correct:} the item is correct, or the precondition ({\tt Where}) is true\\
1.993 +\> {\tt False:} the precondition ({\tt Where}) is false\\
1.994 +\> {\tt Incompl:} the item is incomlete, or not yet input.\\
1.995 +\end{tabbing}
1.996 +
1.997 +
1.998 +
1.999 +\subsection{Refine a problem specification}
1.1000 +The challenge in constructing the problem hierarchy is, to design the branches in such a way, that problem refinement can be done automatically (as it is done in algebra system e.g. by a internal hierarchy of equations).
1.1001 +
1.1002 +For this purpose the hierarchy must be built using the following rules: Let $F$ be a formalization and $P$ and $P_i,\:i=1\cdots n$ problem types, where the $P_i$ are specialized problem types w.r.t. $P$ (i.e. $P$ is a parent node of $P_i$), then
1.1003 +{\small
1.1004 +\begin{enumerate}
1.1005 +\item for all $F$ matching some $P_i$ must follow, that $F$ matches $P$
1.1006 +\item an $F$ matching $P$ should not have more than {\em one} $P_i,\:i=1\cdots n-1$ with $F$ matching $P_i$ (if there are more than one $P_i$, the first one will be taken)
1.1007 +\item for all $F$ matching some $P$ must follow, that $F$ matches $P_n$\\
1.1008 +\end{enumerate}}%small
1.1009 +\noindent Let us give an example for the point (1.) and (2.) first:
1.1010 +{\footnotesize\begin{verbatim}
1.1011 + ML> refine;
1.1012 + val it = fn : fmz -> pblID -> match list
1.1013 + ML>
1.1014 + ML> val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
1.1015 + "solveFor x","errorBound (eps=#0)",
1.1016 + "solutions L"];
1.1017 + ML>
1.1018 + ML> refine fmz ["univariate","equation"];
1.1019 + *** pass ["equation","univariate"]
1.1020 + *** pass ["equation","univariate","linear"]
1.1021 + *** pass ["equation","univariate","plain_square"]
1.1022 + *** pass ["equation","univariate","polynomial"]
1.1023 + *** pass ["equation","univariate","squareroot"]
1.1024 + val it =
1.1025 + [Matches
1.1026 + (["univariate","equation"],
1.1027 + {Find=[Correct "solutions L"],
1.1028 + Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.1029 + Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1.1030 + Where=[Correct
1.1031 + "matches (?a = ?b) (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"],
1.1032 + With=[]}),
1.1033 + NoMatch
1.1034 + (["linear","univariate","equation"],
1.1035 + {Find=[Correct "solutions L"],
1.1036 + Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.1037 + Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1.1038 + Where=[False "(?a + ?b * x = #0) (sqrt (#9 + #4 * x#"],
1.1039 + With=[]}),
1.1040 + NoMatch
1.1041 + (["plain_square","univariate","equation"],
1.1042 + {Find=[Correct "solutions L"],
1.1043 + Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.1044 + Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1.1045 + Where=[False
1.1046 + "matches (?a + ?b * x ^^^ #2 = #0)"],
1.1047 + With=[]}),
1.1048 + NoMatch
1.1049 + (["polynomial","univariate","equation"],
1.1050 + {Find=[Correct "solutions L"],
1.1051 + Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.1052 + Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1.1053 + Where=[False
1.1054 + "is_polynomial_in sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) x"],
1.1055 + With=[]}),
1.1056 + Matches
1.1057 + (["squareroot","univariate","equation"],
1.1058 + {Find=[Correct "solutions L"],
1.1059 + Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.1060 + Correct "solveFor x",Correct "errorBound (eps = #0)"],Relate=[],
1.1061 + Where=[Correct
1.1062 + "contains_root sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) "],
1.1063 + With=[]})] : match list
1.1064 +\end{verbatim}}%size}%footnotesize\label{refine}
1.1065 +This example shows, that in order to refine an {\tt["univariate","equation"]}, the formalization must match respective respective problem type (rule (1.)) and one of the descendants which should match selectively (rule (2.)).
1.1066 +
1.1067 +If no one of the descendants of {\tt["univariate","equation"]} match, rule (3.) comes into play: The {\em last} problem type on this level ($P_n$) provides for a special 'problem type' {\tt["normalize"]}. This node calls a method transforming the equation to a (or another) normal form, which then may match. Look at this example:
1.1068 +{\footnotesize\begin{verbatim}
1.1069 + ML> val fmz = ["equality (x+#1=#2)",
1.1070 + "solveFor x","errorBound (eps=#0)",
1.1071 + "solutions L"];
1.1072 + [...]
1.1073 + ML>
1.1074 + ML> refine fmz ["univariate","equation"];
1.1075 + *** pass ["equation","univariate"]
1.1076 + *** pass ["equation","univariate","linear"]
1.1077 + *** pass ["equation","univariate","plain_square"]
1.1078 + *** pass ["equation","univariate","polynomial"]
1.1079 + *** pass ["equation","univariate","squareroot"]
1.1080 + *** pass ["equation","univariate","normalize"]
1.1081 + val it =
1.1082 + [Matches
1.1083 + (["univariate","equation"],
1.1084 + {Find=[Correct "solutions L"],
1.1085 + Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
1.1086 + Superfl "errorBound (eps = #0)"],Relate=[],
1.1087 + Where=[Correct "matches (?a = ?b) (x + #1 = #2)"],With=[]}),
1.1088 + NoMatch
1.1089 + (["linear","univariate","equation"],
1.1090 + [...]
1.1091 + With=[]}),
1.1092 + NoMatch
1.1093 + (["squareroot","univariate","equation"],
1.1094 + {Find=[Correct "solutions L"],
1.1095 + Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
1.1096 + Correct "errorBound (eps = #0)"],Relate=[],
1.1097 + Where=[False "contains_root x + #1 = #2 "],With=[]}),
1.1098 + Matches
1.1099 + (["normalize","univariate","equation"],
1.1100 + {Find=[Correct "solutions L"],
1.1101 + Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
1.1102 + Superfl "errorBound (eps = #0)"],Relate=[],Where=[],With=[]})]
1.1103 + : match list
1.1104 +\end{verbatim}}%size
1.1105 +The problem type $P_n$, {\tt["normalize","univariate","equation"]}, will transform the equation {\tt x + \#1 = \#2} to the normal form {\tt \#-1 + x = \#0}, which then will match {\tt["linear","univariate","equation"]}.
1.1106 +
1.1107 +This recursive search on the problem hierarchy can be done within a proof state. This leads to the next section.
1.1108 +
1.1109 +
1.1110 +\section{Methods}
1.1111 +A problem type can have one ore more methods solving a respective problem. A method is described by means of another new program language. The language itself looks like a simple functional language, but constructs an imperative proof-state behind the scenes (thus liberating the programer from dealing with technical details and also prohibiting incorrect construction of the proof tree). The interpreter of 'scripts' written in this language evaluates the scriptexpressions, and also delivers certain parts of the script itself for discussion with the user.
1.1112 +
1.1113 +\subsection{The scripts' syntax}
1.1114 +The syntax of scripts follows the definition given in Backus-normal-form:
1.1115 +{\it
1.1116 +\begin{tabbing}
1.1117 +123\=123\=expr ::=\=$|\;\;$\=\kill
1.1118 +\>script ::= {\tt Script} id arg$\,^*$ = body\\
1.1119 +\>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
1.1120 +\>\>body ::= expr\\
1.1121 +\>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
1.1122 +\>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
1.1123 +\>\>\>$|\;$\>listexpr\\
1.1124 +\>\>\>$|\;$\>id\\
1.1125 +\>\>\>$|\;$\>seqex id\\
1.1126 +\>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
1.1127 +\>\>\>$|\;$\>{\tt Repeat} seqex\\
1.1128 +\>\>\>$|\;$\>{\tt Try} seqex\\
1.1129 +\>\>\>$|\;$\>seqex {\tt Or} seqex\\
1.1130 +\>\>\>$|\;$\>seqex {\tt @@} seqex\\
1.1131 +\>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
1.1132 +\>\>type ::= id\\
1.1133 +\>\>tac ::= id
1.1134 +\end{tabbing}}
1.1135 +where {\it id} is an identifier with the usual syntax, {\it prop} is a proposition constructed by Isabelles logical operators (see \cite{Isa-obj} {\tt [isabelle]/src/HOL/HOL.thy}), {\it listexpr} (called {\bf list-expression}) is constructed by Isabelles list functions like {\tt hd, tl, nth} described in {\tt [isabelle]/src/HOL/List.thy}, and {\it type} are (virtually) all types declared in Isabelles version 99.
1.1136 +
1.1137 +Expressions containing some of the keywords {\tt let}, {\tt if} etc. are called {\bf script-expressions}.
1.1138 +
1.1139 +Tactics {\it tac} are (curried) functions. For clarity and simplicity reasons, {\it listexpr} must not contain a {\it tac}, and {\it tac}s must not be nested,
1.1140 +
1.1141 +
1.1142 +\subsection{Control the flow of evaluation}
1.1143 +The flow of control is managed by the following script-expressions called {\it tacticals}.
1.1144 +\begin{description}
1.1145 +\item{{\tt while} prop {\tt Do} expr id}
1.1146 +\item{{\tt if} prop {\tt then} expr {\tt else} expr}
1.1147 +\end{description}
1.1148 +While the the above script-expressions trigger the flow of control by evaluating the current formula, the other expressions depend on the applicability of the tactics within their respective subexpressions (which in turn depends on the proofstate)
1.1149 +\begin{description}
1.1150 +\item{{\tt Repeat} expr id}
1.1151 +\item{{\tt Try} expr id}
1.1152 +\item{expr {\tt Or} expr id}
1.1153 +\item{expr {\tt @@} expr id}
1.1154 +\end{description}
1.1155 +
1.1156 +\begin{description}
1.1157 +\item xxx
1.1158 +
1.1159 +\end{description}
1.1160 +
1.1161 +\section{Do a calculational proof}
1.1162 +First we list all the tactics available so far (this list may be extended during further development of \isac).
1.1163 +
1.1164 +\subsection{Tactics for doing steps in calculations}
1.1165 +\input{tactics}
1.1166 +
1.1167 +\subsection{The functionality of the math engine}
1.1168 +A proof is being started in the math engine {\tt me} by the tactic
1.1169 +\footnote{In the present version a tactic is of type {\tt mstep}.}
1.1170 + {\tt Init\_Proof}, and interactively promoted by other tactics. On input of each tactic the {\tt me} returns the resulting formula and the next tactic applicable. The proof is finished, when the {\tt me} proposes {\tt End\_Proof} as the next tactic.
1.1171 +
1.1172 +We show a calculation (calculational proof) concerning equation solving, where the type of equation is refined automatically: The equation is given by the respective formalization ...
1.1173 +{\footnotesize\begin{verbatim}
1.1174 + ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
1.1175 + "errorBound (eps=#0)","solutions L"];
1.1176 + val fmz =
1.1177 + ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
1.1178 + "solutions L"] : string list
1.1179 + ML>
1.1180 + ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
1.1181 + ("SqRoot.thy","no_met"));
1.1182 + val dom = "SqRoot.thy" : string
1.1183 + val pbt = ["univariate","equation"] : string list
1.1184 + val met = ("SqRoot.thy","no_met") : string * string
1.1185 +\end{verbatim}}%size
1.1186 +... and the specification {\tt spec} of a domain {\tt dom}, a problem type {\tt pbt} and a method {\tt met}. Note that the equation is such, that it is not immediatly clear, what type it is in particular (it could be a polynomial of degree 2; but, for sure, the type is some specialized type of a univariate equation). Thus, no method ({\tt no\_met}) can be specified for solving the problem.
1.1187 +
1.1188 +Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types.
1.1189 +
1.1190 +
1.1191 +\subsection{Initialize the calculation}
1.1192 +The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ptree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons.
1.1193 +{\footnotesize\begin{verbatim}
1.1194 + ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
1.1195 + val mID = "Init_Proof" : string
1.1196 + val m =
1.1197 + Init_Proof
1.1198 + (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
1.1199 + "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep
1.1200 + ML>
1.1201 + ML> val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;
1.1202 + val p = ([],Pbl) : pos'
1.1203 + val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
1.1204 + val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1.1205 + : string * mstep
1.1206 + val pt =
1.1207 + Nd
1.1208 + (PblObj
1.1209 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1.1210 + result=#,spec=#},[]) : ptree
1.1211 + \end{verbatim}}%size
1.1212 +The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ptree}, {\tt pos'}).
1.1213 +
1.1214 +We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:
1.1215 +{\footnotesize\begin{verbatim}
1.1216 + ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
1.1217 + val it = () : unit
1.1218 + ML>
1.1219 + ML> f;
1.1220 + val it =
1.1221 + Form'
1.1222 + (PpcKF
1.1223 + (0,EdUndef,0,Nundef,
1.1224 + (Problem [],
1.1225 + {Find=[Incompl "solutions []"],
1.1226 + Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
1.1227 + Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
1.1228 +\end{verbatim}}%size
1.1229 +Recall, please, the format of a problem as presented in sect.\ref{pbl} on p.\pageref{pbl}; such an 'empty' problem can be found above encapsulated by several constructors containing additional data (necessary for the dialog guide, not relevant here).\\
1.1230 +
1.1231 +{\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\
1.1232 +
1.1233 +In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user.
1.1234 +{\footnotesize\begin{verbatim}
1.1235 + ML> nxt;
1.1236 + val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1.1237 + : string * mstep
1.1238 + ML>
1.1239 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1240 + val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])
1.1241 + : string * mstep
1.1242 + ML>
1.1243 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1244 +\end{verbatim}}%size
1.1245 +
1.1246 +
1.1247 +\subsection{The phase of modeling}
1.1248 +comprises the input of the items of the problem; the {\tt me} can help by use of the formalization tacitly transferred by {\tt Init\_Proof}. In particular, the {\tt me} in general 'knows' the next promising tactic; the first one has been returned by the (hidden) tactic {\tt Model\_Problem}.
1.1249 +
1.1250 +{\footnotesize\begin{verbatim}
1.1251 + ML> nxt;
1.1252 + val it =
1.1253 + ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
1.1254 + : string * mstep
1.1255 + ML>
1.1256 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1257 + val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep
1.1258 + ML>
1.1259 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1260 + val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep
1.1261 + ML>
1.1262 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1263 + val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
1.1264 +\end{verbatim}}%size
1.1265 +\noindent Now the problem is 'modeled', all items are input. We convince ourselves by increasing {\tt Compiler.Control.Print.printDepth} once more.
1.1266 +{\footnotesize\begin{verbatim}
1.1267 + ML> Compiler.Control.Print.printDepth:=8;
1.1268 + ML> f;
1.1269 + val it =
1.1270 + Form'
1.1271 + (PpcKF
1.1272 + (0,EdUndef,0,Nundef,
1.1273 + (Problem [],
1.1274 + {Find=[Correct "solutions L"],
1.1275 + Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.1276 + Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
1.1277 +\end{verbatim}}%size
1.1278 +%One of the input items is considered {\tt Superfluous} by the {\tt me} consulting the problem type {\tt ["univariate","equation"]}. The {\tt ErrorBound}, however, could become important in case the equation only could be solved by some iteration method.
1.1279 +
1.1280 +\subsection{The phase of specification}
1.1281 +This phase provides for explicit determination of the domain, the problem type, and the method to be used. In particular, the search for the appropriate problem type is being supported. There are two tactics for this purpose: {\tt Specify\_Problem} generates feedback on how a candidate of a problem type matches the current problem, and {\tt Refine\_Problem} provides help by the system, if the user gets lost.
1.1282 +{\footnotesize\begin{verbatim}
1.1283 +ML> nxt;
1.1284 + val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
1.1285 + ML>
1.1286 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1287 + val nxt =
1.1288 + ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"])
1.1289 + : string * mstep
1.1290 + val pt =
1.1291 + Nd
1.1292 + (PblObj
1.1293 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1.1294 + result=#,spec=#},[]) : ptree
1.1295 +\end{verbatim}}%size
1.1296 +The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows.
1.1297 +{\footnotesize\begin{verbatim}
1.1298 + ML> val nxt = ("Specify_Problem",
1.1299 + Specify_Problem ["polynomial","univariate","equation"]);
1.1300 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1301 + val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
1.1302 + val nxt =
1.1303 + ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"])
1.1304 + : string * mstep
1.1305 + ML>
1.1306 + ML> val nxt = ("Specify_Problem",
1.1307 + Specify_Problem ["linear","univariate","equation"]);
1.1308 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1309 + val f =
1.1310 + Form'
1.1311 + (PpcKF
1.1312 + (0,EdUndef,0,Nundef,
1.1313 + (Problem ["linear","univariate","equation"],
1.1314 + {Find=[Correct "solutions L"],
1.1315 + Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.1316 + Correct "solveFor x"],Relate=[],
1.1317 + Where=[False
1.1318 + "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1.1319 + With=[]}))) : mout
1.1320 +\end{verbatim}}%size
1.1321 +Again assuming that the dialog guide hide the next tactic proposed by the {\tt me}, and the student gets lost, {\tt Refine\_Problem} always 'knows' the way out, if applied to the problem type {\tt["univariate","equation"]}.
1.1322 +{\footnotesize\begin{verbatim}
1.1323 + ML> val nxt = ("Refine_Problem",
1.1324 + Refine_Problem ["linear","univariate","equation
1.1325 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1326 + val f = Problems (RefinedKF [NoMatch #]) : mout
1.1327 + ML>
1.1328 + ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1.1329 + val f =
1.1330 + Problems
1.1331 + (RefinedKF
1.1332 + [NoMatch
1.1333 + (["linear","univariate","equation"],
1.1334 + {Find=[Correct "solutions L"],
1.1335 + Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.1336 + Correct "solveFor x"],Relate=[],
1.1337 + Where=[False
1.1338 + "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1.1339 + With=[]})]) : mout
1.1340 + ML>
1.1341 + ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
1.1342 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1343 + val f =
1.1344 + Problems
1.1345 + (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])
1.1346 + : mout
1.1347 + ML>
1.1348 + ML>
1.1349 + ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1.1350 + val f =
1.1351 + Problems
1.1352 + (RefinedKF
1.1353 + [Matches
1.1354 + (["univariate","equation"],
1.1355 + {Find=[Correct "solutions L"],
1.1356 + Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.1357 + Correct "solveFor x"],Relate=[],
1.1358 + Where=[Correct
1.1359 + With=[]}),
1.1360 + NoMatch
1.1361 + (["linear","univariate","equation"],
1.1362 + {Find=[Correct "solutions L"],
1.1363 + Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.1364 + Correct "solveFor x"],Relate=[],
1.1365 + Where=[False
1.1366 + "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1.1367 + With=[]}),
1.1368 + NoMatch
1.1369 + ...
1.1370 + ...
1.1371 + Matches
1.1372 + (["normalize","univariate","equation"],
1.1373 + {Find=[Correct "solutions L"],
1.1374 + Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.1375 + Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
1.1376 +\end{verbatim}}%size
1.1377 +The tactic {\tt Refine\_Problem} returns all matches to problem types along the path traced in the problem hierarchy (anlogously to the authoring tool for refinement in sect.\ref{refine} on p.\pageref{refine}) --- a lot of information to be displayed appropriately in the hiearchy browser~!
1.1378 +
1.1379 +\subsection{The phase of solving}
1.1380 +This phase starts by invoking a method, which acchieves the normal form within two tactics, {\tt Rewrite rnorm\_equation\_add} and {\tt Rewrite\_Set SqRoot\_simplify}:
1.1381 +{\footnotesize\begin{verbatim}
1.1382 + ML> nxt;
1.1383 + val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
1.1384 + : string * mstep
1.1385 + ML>
1.1386 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1387 + val f =
1.1388 + Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8"))
1.1389 + val nxt =
1.1390 + ("Rewrite", Rewrite
1.1391 + ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)"))
1.1392 + ML>
1.1393 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1394 + val f =
1.1395 + Form' (FormKF (~1,EdUndef,1,Nundef,
1.1396 + "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout
1.1397 + val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep
1.1398 + ML>
1.1399 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1400 + val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
1.1401 + val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
1.1402 +\end{verbatim}}%size
1.1403 +Now the normal form {\tt \#-6 + \#3 * x = \#0} is the input to a subproblem, which again allows for specification of the type of equation, and the respective method:
1.1404 +{\footnotesize\begin{verbatim}
1.1405 + ML> nxt;
1.1406 + val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1.1407 + ML>
1.1408 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1409 + val f =
1.1410 + Form' (FormKF
1.1411 + (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])"))
1.1412 + : mout
1.1413 + val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1.1414 + ML>
1.1415 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1416 + val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
1.1417 +\end{verbatim}}%size
1.1418 +As required, the tactic {\tt Refine ["univariate","equation"]} selects the appropriate type of equation from the problem hierarchy, which can be seen by the tactic {\tt Model\_Problem ["linear","univariate","equation"]} prosed by the system.
1.1419 +
1.1420 +Again the whole phase of modeling and specification follows; we skip it here, and \isac's dialog guide may decide to do so as well.
1.1421 +
1.1422 +
1.1423 +\subsection{The final phase: check the post-condition}
1.1424 +The type of problems solved by \isac{} are so-called 'example construction problems' as shown above. The most characteristic point of such a problem is the post-condition. The handling of the post-condition in the given context is an open research question.
1.1425 +
1.1426 +Thus the post-condition is just mentioned, in our example for both, the problem and the subproblem:
1.1427 +{\footnotesize\begin{verbatim}
1.1428 + ML> nxt;
1.1429 + val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
1.1430 + ML>
1.1431 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1432 + val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout
1.1433 + val nxt =
1.1434 + ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"])
1.1435 + ML>
1.1436 + ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.1437 + val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
1.1438 + val nxt = ("End_Proof'",End_Proof') : string * mstep
1.1439 +\end{verbatim}}%size
1.1440 +The next tactic proposed by the system, {\tt End\_Proof'} indicates that the proof has finished successfully.\\
1.1441 +
1.1442 +{\it The tactics proposed by the system need {\em not} be followed by the user; the user is free to choose other tactics, and the system will report, if this is applicable at the respective proof state, or not~! The reader may try out~!}
1.1443 +
1.1444 +
1.1445 +
1.1446 +\chapter{Systematic description}
1.1447 +
1.1448 +
1.1449 +\section{The structure of the knowledge base}
1.1450 +
1.1451 +\subsection{Tactics and data}
1.1452 +First we view the ME from outside, i.e. we regard tactics and relate them to the knowledge base (KB). W.r.t. the KB we address the atomic items which have to be implemented in detail by the authors of the KB
1.1453 +\footnote{Some of these items are fetched by the tactics from intermediate storage within the ME, and not directly from the KB.}
1.1454 +. The items are listed in alphabetical order in Tab.\ref{kb-items} on p.\pageref{kb-items}.
1.1455 +{\begin{table}[h]
1.1456 +\caption{Atomic items of the KB} \label{kb-items}
1.1457 +%\tabcolsep=0.3mm
1.1458 +\begin{center}
1.1459 +\def\arraystretch{1.0}
1.1460 +\begin{tabular}{lp{9.0cm}}
1.1461 +abbrevation & description \\
1.1462 +\hline
1.1463 +&\\
1.1464 +{\it calc\_list}
1.1465 +& associationlist of the evaluation-functions {\it eval\_fn}\\
1.1466 +{\it eval\_fn}
1.1467 +& evaluation-function for numerals and for predicates coded in SML\\
1.1468 +{\it eval\_rls }
1.1469 +& ruleset {\it rls} for simplifying expressions with {\it eval\_fn}s\\
1.1470 +{\it fmz}
1.1471 +& formalization, i.e. a minimal formula representation of an example \\
1.1472 +{\it met}
1.1473 +& a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it scr}, etc.)\\
1.1474 +{\it metID}
1.1475 +& reference to a {\it met}\\
1.1476 +{\it op}
1.1477 +& operator as key to an {\it eval\_fn} in a {\it calc\_list}\\
1.1478 +{\it pbl}
1.1479 +& problem, i.e. a node in the problem-hierarchy\\
1.1480 +{\it pblID}
1.1481 +& reference to a {\it pbl}\\
1.1482 +{\it rew\_ord}
1.1483 +& rewrite-order\\
1.1484 +{\it rls}
1.1485 +& ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\
1.1486 +{\it Rrls}
1.1487 +& ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\
1.1488 +{\it scr}
1.1489 +& script describing algorithms by tactics, part of a {\it met} \\
1.1490 +{\it norm\_rls}
1.1491 +& special ruleset calculating a normalform, associated with a {\it thy}\\
1.1492 +{\it spec}
1.1493 +& specification, i.e. a tripel ({\it thyID, pblID, metID})\\
1.1494 +{\it subs}
1.1495 +& substitution, i.e. a list of variable-value-pairs\\
1.1496 +{\it term}
1.1497 +& Isabelle term, i.e. a formula\\
1.1498 +{\it thm}
1.1499 +& theorem\\
1.1500 +{\it thy}
1.1501 +& theory\\
1.1502 +{\it thyID}
1.1503 +& reference to a {\it thy} \\
1.1504 +\end{tabular}\end{center}\end{table}
1.1505 +}
1.1506 +The relations between tactics and data items are shown in Tab.\ref{tac-kb}on p.\pageref{tac-kb}.
1.1507 +{\def\arraystretch{1.2}
1.1508 +\begin{table}[h]
1.1509 +\caption{Which tactic uses which KB's item~?} \label{tac-kb}
1.1510 +\tabcolsep=0.3mm
1.1511 +\begin{center}
1.1512 +\begin{tabular}{|ll||cccc|ccc|cccc|} \hline
1.1513 +tactic &input & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1.1514 + & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1.1515 +\hline\hline
1.1516 +Init\_Proof
1.1517 + &fmz & x & & & x & & & & & & & x \\
1.1518 + &spec & & & & & & & & & & & \\
1.1519 +\hline
1.1520 +\multicolumn{13}{|l|}{model phase}\\
1.1521 +\hline
1.1522 +Add\_* &term & x & & & x & & & & & & & x \\
1.1523 +FormFK &model & x & & & x & & & & & & & x \\
1.1524 +\hline
1.1525 +\multicolumn{13}{|l|}{specify phase}\\
1.1526 +\hline
1.1527 +Specify\_Theory
1.1528 + &thyID & x & & & x & & & & x & x & & x \\
1.1529 +Specify\_Problem
1.1530 + &pblID & x & & & x & & & & x & x & & x \\
1.1531 +Refine\_Problem
1.1532 + &pblID & x & & & x & & & & x & x & & x \\
1.1533 +Specify\_Method
1.1534 + &metID & x & & & x & & & & x & x & & x \\
1.1535 +Apply\_Method
1.1536 + &metID & x & x & & x & & & & x & x & & x \\
1.1537 +\hline
1.1538 +\multicolumn{13}{|l|}{solve phase}\\
1.1539 +\hline
1.1540 +Rewrite,\_Inst
1.1541 + &thm & x & x & & & x &met & & x &met & & \\
1.1542 +Rewrite, Detail
1.1543 + &thm & x & x & & & x &rls & & x &rls & & \\
1.1544 +Rewrite, Detail
1.1545 + &thm & x & x & & & x &Rrls & & x &Rrls & & \\
1.1546 +Rewrite\_Set,\_Inst
1.1547 + &rls & x & x & & & & & x & x & x & & \\
1.1548 +Calculate
1.1549 + &op & x & x & & & & & & & & x & \\
1.1550 +Substitute
1.1551 + &subs & x & & & x & & & & & & & \\
1.1552 + & & & & & & & & & & & & \\
1.1553 +SubProblem
1.1554 + &spec & x & x & & x & & & & x & x & & x \\
1.1555 + &fmz & & & & & & & & & & & \\
1.1556 +\hline
1.1557 +\end{tabular}\end{center}\end{table}
1.1558 +}
1.1559 +
1.1560 +\subsection{\isac's theories}
1.1561 +\isac's theories build upon Isabelles theories for high-order-logic (HOL) up to the respective development of real numbers ({\tt HOL/Real}). Theories have a special format defined in \cite{Isa-ref} and the suffix {\tt *.thy}; usually theories are paired with SML-files having the same filename and the suffix {\tt *.ML}.
1.1562 +
1.1563 +\isac's theories represent the deductive part of \isac's knowledge base, the hierarchy of theories is structured accordingly. The {\tt *.ML}-files, however, contain {\em all} data of the other two axes of the knowledge base, the problems and the methods (without presenting their respective structure, which is done by the problem browser and the method browser, see \ref{pbt}).
1.1564 +
1.1565 +Tab.\ref{theories} on p.\pageref{theories} lists the basic theories planned to be implemented in version \isac.1. We expext the list to be expanded in the near future, actually, have a look to the theory browser~!
1.1566 +
1.1567 +The first three theories in the list do {\em not} belong to \isac's knowledge base; they are concerned with \isac's script-language for methods and listed here for completeness.
1.1568 +{\begin{table}[h]
1.1569 +\caption{Theories in \isac-version I} \label{theories}
1.1570 +%\tabcolsep=0.3mm
1.1571 +\begin{center}
1.1572 +\def\arraystretch{1.0}
1.1573 +\begin{tabular}{lp{9.0cm}}
1.1574 +theory & description \\
1.1575 +\hline
1.1576 +&\\
1.1577 +ListI.thy
1.1578 +& assigns identifiers to the functions defined in {\tt Isabelle2002/src/HOL/List.thy} and (intermediatly~?) defines some more list functions\\
1.1579 +ListI.ML
1.1580 +& {\tt eval\_fn} for the additional list functions\\
1.1581 +Tools.thy
1.1582 +& functions required for the evaluation of scripts\\
1.1583 +Tools.ML
1.1584 +& the respective {\tt eval\_fn}s\\
1.1585 +Script.thy
1.1586 +& prerequisites for scripts: types, tactics, tacticals,\\
1.1587 +Script.ML
1.1588 +& sets of tactics and functions for internal use\\
1.1589 +& \\
1.1590 +\hline
1.1591 +& \\
1.1592 +Typefix.thy
1.1593 +& an intermediate hack for escaping type errors\\
1.1594 +Descript.thy
1.1595 +& {\it description}s for the formulas in {\it model}s and {\it problem}s\\
1.1596 +Atools
1.1597 +& (re-)definition of operators; general predicates and functions for preconditions; theorems for the {\tt eval\_rls}\\
1.1598 +Float
1.1599 +& floating point numerals\\
1.1600 +Equation
1.1601 +& basic notions for equations and equational systems\\
1.1602 +Poly
1.1603 +& polynomials\\
1.1604 +PolyEq
1.1605 +& polynomial equations and equational systems \\
1.1606 +Rational.thy
1.1607 +& additional theorems for rationals\\
1.1608 +Rational.ML
1.1609 +& cancel, add and simplify rationals using (a generalization of) Euclids algorithm; respective reverse rulesets\\
1.1610 +RatEq
1.1611 +& equations on rationals\\
1.1612 +Root
1.1613 +& radicals; calculate normalform; respective reverse rulesets\\
1.1614 +RootEq
1.1615 +& equations on roots\\
1.1616 +RatRootEq
1.1617 +& equations on rationals and roots (i.e. on terms containing both operations)\\
1.1618 +Vect
1.1619 +& vector analysis\\
1.1620 +Trig
1.1621 +& trigonometriy\\
1.1622 +LogExp
1.1623 +& logarithms and exponential functions\\
1.1624 +Calculus
1.1625 +& nonstandard analysis\\
1.1626 +Diff
1.1627 +& differentiation\\
1.1628 +DiffApp
1.1629 +& applications of differentiaten (maxima-minima-problems)\\
1.1630 +Test
1.1631 +& (old) data for the test suite\\
1.1632 +Isac
1.1633 +& collects all \isac-theoris.\\
1.1634 +\end{tabular}\end{center}\end{table}
1.1635 +}
1.1636 +
1.1637 +
1.1638 +\subsection{Data in {\tt *.thy}- and {\tt *.ML}-files}
1.1639 +As already mentioned, theories come in pairs of {\tt *.thy}- and {\tt *.ML}-files with the same respective filename. How data are distributed between the two files is shown in Tab.\ref{thy-ML} on p.\pageref{thy-ML}.
1.1640 +{\begin{table}[h]
1.1641 +\caption{Data in {\tt *.thy}- and {\tt *.ML}-files} \label{thy-ML}
1.1642 +\tabcolsep=2.0mm
1.1643 +\begin{center}
1.1644 +\def\arraystretch{1.0}
1.1645 +\begin{tabular}{llp{7.7cm}}
1.1646 +file & data & description \\
1.1647 +\hline
1.1648 +& &\\
1.1649 +{\tt *.thy}
1.1650 +& consts
1.1651 +& operators, predicates, functions, script-names ('{\tt Script} name \dots{\tt arguments}')
1.1652 +\\
1.1653 +& rules
1.1654 +& theorems: \isac{} uses Isabelles theorems if possible; additional theorems analoguous to such existing in Isabelle get the Isabelle-identifier attached an {\it I}
1.1655 +\\& &\\
1.1656 +{\tt *.ML}
1.1657 +& {\tt theory' :=}
1.1658 +& the theory defined by the actual {\tt *.thy}-file is made accessible to \isac
1.1659 +\\
1.1660 +& {\tt eval\_fn}
1.1661 +& evaluation function for operators and predicates, coded on the meta-level (SML); the identifier of such a function is a combination of the keyword {\tt eval\_} with the identifier of the function as defined in {\tt *.thy}
1.1662 +\\
1.1663 +& {\tt *\_simplify}
1.1664 +& the canonical simplifier for the actual theory, i.e. the identifier for this ruleset is a combination of the theories identifier and the keyword {\tt *\_simplify}
1.1665 +\\
1.1666 +& {\tt norm\_rls :=}
1.1667 +& the canonical simplifier {\tt *\_simplify} is stored such that it is accessible for \isac
1.1668 +\\
1.1669 +& {\tt rew\_ord' :=}
1.1670 +& the same for rewrite orders, if needed outside of one particular ruleset
1.1671 +\\
1.1672 +& {\tt ruleset' :=}
1.1673 +& the same for rulesets (ordinary rulesets, reverse rulesets and {\tt eval\_rls})
1.1674 +\\
1.1675 +& {\tt calc\_list :=}
1.1676 +& the same for {\tt eval\_fn}s, if needed outside of one particular ruleset (e.g. for a tactic {\tt Calculate} in a script)
1.1677 +\\
1.1678 +& {\tt store\_pbl}
1.1679 +& problems defined within this {\tt *.ML}-file are made accessible for \isac
1.1680 +\\
1.1681 +& {\tt methods :=}
1.1682 +& methods defined within this {\tt *.ML}-file are made accessible for \isac
1.1683 +\\
1.1684 +\end{tabular}\end{center}\end{table}
1.1685 +}
1.1686 +The order of the data-items within the theories should adhere to the order given in this list.
1.1687 +
1.1688 +\subsection{Formal description of the problem-hierarchy}
1.1689 +%for Richard Lang
1.1690 +
1.1691 +\subsection{Script tactics}
1.1692 +The tactics actually promote the calculation: they construct the prooftree behind the scenes, and they are the points during evaluation where the script-interpreter transfers control to the user. Here we only describe the sytax of the tactics; the semantics is described on p.\pageref{user-tactics} below in context with the tactics the student uses ('user-tactics'): there is a 1-to-1 correspondence between user-tactics and script-tactics.
1.1693 +
1.1694 +
1.1695 +
1.1696 +
1.1697 +
1.1698 +\chapter{Authoring on the knowledge}
1.1699 +
1.1700 +
1.1701 +\subsection{Add a theorem}
1.1702 +\subsection{Define and add a problem}
1.1703 +\subsection{Define and add a predicate}
1.1704 +\subsection{Define and add a method}
1.1705 +\subsection{}
1.1706 +\subsection{}
1.1707 +\subsection{}
1.1708 +\subsection{}
1.1709 +
1.1710 +
1.1711 +
1.1712 +\newpage
1.1713 +%\bibliography{math-eng} %for graz
1.1714 +\bibliography{doc}
1.1715 +
1.1716 +\end{document}
1.1717 \ No newline at end of file
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc/sdd-content.tex Thu Apr 17 18:01:02 2003 +0200
2.3 @@ -0,0 +1,931 @@
2.4 +%nicht vergessen: auch sdd.tex ($Revision $) \"andern !
2.5 +\chapter{Software Design Document}
2.6 +
2.7 +
2.8 +\section{The Worksheet}
2.9 +%WN --- vvv -----------------Kopie aus UseCases am 2.9.02-----------------
2.10 +The worksheet is the component responsible for interaction with the user while doing a claculation.
2.11 +
2.12 +The functionality is split between a worksheet presentation layer (WPL) and the worksheet dialog guide (WDG). This makes it possible to change the logic of user-interaction (WDG) and the presentation or skin (WPL) independently from each other.
2.13 +
2.14 +The WPL is responsible for visible presentation of data (like formulas in a calculation) and user-interface objects (like buttons or menus). Moreover, the WPL accepts input from the user.
2.15 +The WDG makes decisions on which data and which choices of user-interaction to present in which order, depending on the role (student, teacher, author, ...), the preferences and the history of the user.
2.16 +
2.17 +\subsection{Elements of user-interaction}
2.18 +
2.19 +Any of the following elements can be activated by the user (e.g. clicked with a mouse) to get a choice of actions offered for the respective item. The actions available are determined by the WDG. The choice can be empty as well.
2.20 +\begin{itemize}
2.21 +\item \textbf{Menus} in the usual sense of the word are filled in by the WDG. Several "types" of menus will be offered, including:
2.22 +\begin{itemize}
2.23 +\item global settings
2.24 +\item display options
2.25 +\item calculation options
2.26 +\item user profile
2.27 +\end{itemize}
2.28 +\item \textbf{Formulas} are the visual representation of mathematical formulas.
2.29 +Actions offered on formulas include:
2.30 +\begin{itemize}
2.31 +\item Edit
2.32 +\item Collapse (minimize) / Show
2.33 +\item Propose a tactic
2.34 +\item Make current
2.35 +\item Highlight
2.36 +\end{itemize}
2.37 +\item \textbf{Tactics} are rules applied to a formula yielding another formula (the next formula in the course of calculation).
2.38 +Actions offered on tactics include:
2.39 +\begin{itemize}
2.40 +\item Edit
2.41 +\item Choose from list of applicable tactics
2.42 +\item Get information from knowledge base
2.43 +\end{itemize}
2.44 +\end{itemize}
2.45 +
2.46 +\subsection{Data stored and manipulated by the WDG}
2.47 +\subsubsection{Draft for an user-model}
2.48 +The user-model stores an abstraction of the knowledge, abilities and learning progress of a user, based upon his history of interaction with \isac{} as well as his personal preferences and restrictions set by teachers and course designers. The user-model is persistent across sessions.
2.49 +
2.50 +At the moment, the uses of the user-model and the implications for the data abstractions stored cannot be foreseen in every detail. To avoid prejudicing decisions to be taken by dialog designers, the user model is designed to store data at a rather low level of abstraction suitable for being combined into high-level equivalents at a later time. Moreover, a mechanism transparent to future extensions is preferred.
2.51 +
2.52 +Elements of the user model envisioned at present include:
2.53 +\begin{itemize}
2.54 +\item \textbf{Specific examples already done by the user} will be logged together with information about success or failure. This "history" can be used to deduce flexible strategies for user-guidance.
2.55 +\item \textbf{Errors typical to the user} will be included as soon as a comprehensive classification of common errors is implemented in the system. This information can be used to automatically choose specific examples to be practised.
2.56 +\item \textbf{Tactics considered no longer interesting to the user} will be used to reduce the complexity of user-interaction by omitting steps in the calculation trivial to the specific user. Tactics having been applied several times withot error could be considered trivial in this sense of the word.
2.57 +\item \textbf{Tactics to be practised by the user} will be used to choose specific examples or to leave parts of the calculation blank to be filled in by the user.
2.58 +\item \textbf{Specific examples to be done by the user}
2.59 +\end{itemize}
2.60 +Preferences about the visual representation such as colors, fonts or visual layout of the worksheet depend heavily on the capabilities of the WPL and will be stored separately.
2.61 +Depending on the role and permissions of the user, some of these user-model data could be set directly by the user according to his preferences, whereas othe data may be modified only by the system or a privileged teacher.
2.62 +
2.63 +\subsubsection{Dialog state}
2.64 +The dialog state stores the momentary state of interaction in the current session.
2.65 +
2.66 +\subsection{The object world of the worksheet component}
2.67 +
2.68 +\subsubsection{The dialog guide object}
2.69 +Its local data represent the current state of the dialog. It has methods for interacting with the user at different levels of abstraction and for being queried about its interpretation of the proof tree.
2.70 +
2.71 +\subsubsection{The user model object}
2.72 +
2.73 +\subsubsection{The presentation layer object}
2.74 +The presentation layer object is an abstraction of the visible worksheet.
2.75 +It has methods for
2.76 +\begin{itemize}
2.77 +\item redisplaying itself
2.78 +\item showing menus, buttons and other objects of user-interaction
2.79 +\item highlighting parts of the displayed calculation
2.80 +\item editing the hot spot of the calculation
2.81 +\item being notified of changes in the data displayed
2.82 +\end{itemize}
2.83 +It does not have methods for directly changing the data displayed, but reacts to update notifications by re-querying the data.
2.84 +It notifies other objects of
2.85 +\begin{itemize}
2.86 +\item actions (e.g. mouse clicks) on the displayed elements
2.87 +\item completed edit operations
2.88 +\end{itemize}
2.89 +
2.90 +\subsubsection{The proof tree object}
2.91 +The proof tree object represents a proof or course of calculation, consisting of a problem specification and a series of formulas an tactics.
2.92 +It has methods for
2.93 +\begin{itemize}
2.94 +\item being initialized with a problem specification
2.95 +\item checking a problem specification for completeness and consistency
2.96 +\item being queried about its inner structure (i.e. formulas and tactics)
2.97 +\item changing itself by doing steps in a calculation
2.98 +\item changing itself by adding detail to a step in the calculation, leaving the rest of the tree consistent and unchanged
2.99 +\item finding the origins of conditions, yielding highlights indicating the tactics which introduced a condition
2.100 +\item setting the hot spot, i.e. the current formula or tactic
2.101 +\item changing the data at the hot spot and verifying the consistency of the resulting proof
2.102 +\end{itemize}
2.103 +It can notify other objects of updates, optionally indicating parts of the tree left unchanged.
2.104 +
2.105 +\subsubsection{The proof element selector object}
2.106 +The proof element selector object is intended for selecting a formula or a tactic in a proof. Its implementation is closely interwoven with the proof tree object.
2.107 +It has methods for
2.108 +\begin{itemize}
2.109 +\item attaching and detaching a proof tree
2.110 +\item navigating the attached proof tree, i.e. selecting a formula or tactic. Navigation is done by methods like the following
2.111 +\begin{itemize}
2.112 +\item root - select the first formula
2.113 +\item down - select the next formula
2.114 +\item up - select previous formula
2.115 +\item tactic - select the tactic yielding the currently selected formula
2.116 +\item formula - select the formula resulting from the currently selected tactic
2.117 +\end{itemize}
2.118 +\item extracting the selected formula yielding a new formula object
2.119 +\item extracting the selected tactic yielding a new tactic object
2.120 +\end{itemize}
2.121 +
2.122 +
2.123 +\subsubsection{The formula object}
2.124 +The formula object is intended for storing one mathematical formula, i.e. a term consisting of constants, variables, operators and functions.
2.125 +While the internal storage is not transparent to the outside and follows requirements of the implementation, the object has methods for storing and retrieving the formula in at least two formats:
2.126 +\begin{itemize}
2.127 +\item retrieve the formula in MathML content format
2.128 +\item store the formula in MathML content format
2.129 +\item retrieve the formula in isabelle text format
2.130 +\item store the formula in isabelle text format
2.131 +\item given a subterm selector, retrieve the formula in MathML content format leaving the selected subterm blank for being filled in by the user
2.132 +\end{itemize}
2.133 +Other formats can be supported by adding respective store/retrieve methods.
2.134 +
2.135 +\subsubsection{The subterm selector object}
2.136 +The subterm selector object is intended for selecting a subterm of a formula. Its implementation is closely interwoven with the formula object.
2.137 +It has methods for
2.138 +\begin{itemize}
2.139 +\item attaching and detaching a formula
2.140 +\item navigating the attached formula, i.e. selecting different subterms. Navigation is done by methods like the following (please imagine the term being stored in a tree structure with operators as nodes and variables \& constants as leaves).
2.141 +\begin{itemize}
2.142 +\item root - select the whole term
2.143 +\item down - select the leftmost subterm of the currently selected term
2.144 +\item up - select the superterm of the currently selected term
2.145 +\item left - select the previous term on the same level
2.146 +\item right - select the next term on the same level
2.147 +\end{itemize}
2.148 +\item extracting the selected formula yielding a new formula object
2.149 +\end{itemize}
2.150 +
2.151 +\subsubsection{The tactic object}
2.152 +The tactic object stores a rule for transforming one formula into another.
2.153 +Methods implemented include:
2.154 +\begin{enumerate}
2.155 +\item retrieve the name of the tactic
2.156 +\item retrieve a short description of the tactic
2.157 +\item retrieve a formula illustrating the tactic, if available
2.158 +\item given a formula \textit{f} the tactic is applied to, retrieve a formula illustrating the application of the tactic on \textit{f}
2.159 +\end{enumerate}
2.160 +
2.161 +\subsubsection{The problem specification object}
2.162 +
2.163 +\subsubsection{The menu object}
2.164 +
2.165 +\subsubsection{The worksheet highlight object}
2.166 +The worksheet highlight object is to the proof displayed on the worksheet what the proof element seletor object is to the proof tree. It is not yet clear whether both objects can be merged into one.
2.167 +
2.168 +\subsection{Interfacing with the worksheet}
2.169 +
2.170 +\subsection{Interface WPL-WDG}
2.171 +
2.172 +\subsubsection{Actions executed by the WPL on behalf of the WDG}
2.173 +\begin{itemize}
2.174 +\item \textbf{Redisplay tree}
2.175 +\item \textbf{Set active formula}
2.176 +\item \textbf{Highlight parts of the calculation}
2.177 +\item \textbf{Expand or collapse parts of the calculation}
2.178 +\item \textbf{Edit the current formula}
2.179 +\item \textbf{Choose a tactic from a list of applicable tactics}
2.180 +\item \textbf{Choose a tactic from the knowledge base}
2.181 +\item \textbf{Open Knowledge Browser}
2.182 +\item \textbf{Offer a menu of choices}
2.183 +\end{itemize}
2.184 +
2.185 +\subsubsection{User events passed from WPL to WDG}
2.186 +\begin{itemize}
2.187 +\item \textbf{Editing of formula completed}
2.188 +\item \textbf{Editing of tactic completed}
2.189 +\item \textbf{Menu item selected}
2.190 +
2.191 +\end{itemize}
2.192 +
2.193 +\subsection{Interface WDG-ME}
2.194 +
2.195 +\subsubsection{Actions executed by the ME on behalf of the WDG}
2.196 +Actions related to a specific calculation (proof-tree):
2.197 +\begin{itemize}
2.198 +\item \textbf{Set active formula}
2.199 +\item \textbf{Modifiy active formula}
2.200 +\item \textbf{Set next tactic}
2.201 +\item \textbf{Calculate one step}
2.202 +Apply the current tactic.
2.203 +\item \textbf{Calculate to the end of the current sub-problem}
2.204 +\item \textbf{Calculate to the end of the current problem}
2.205 +\item \textbf{Find origin of a condition}
2.206 +\end{itemize}
2.207 +
2.208 +Actions not related to a specific calculation (proof-tree):
2.209 +\begin{itemize}
2.210 +\item \textbf{Initialize calculation with a problem specification}
2.211 +\item \textbf{Mark parts of a formula suitable for being filled in by the student}
2.212 +\end{itemize}
2.213 +
2.214 +\subsubsection{Calculational events passed from ME to WDG}
2.215 +\begin{itemize}
2.216 +\item \textbf{Tree updated}
2.217 +\item \textbf{Calculation completed}
2.218 +Success.
2.219 +\item \textbf{Failure/Error condition}
2.220 +\end{itemize}
2.221 +
2.222 +\subsection{Interface WDG-Knowledge Browser}
2.223 +The WDG and the Knowledge Browser communicate at a rather high level of abstraction, contacting an instance of the other component and setting a starting point for further action.
2.224 +
2.225 +\subsubsection{WDG used by the Knowledge Browser}
2.226 +\begin{itemize}
2.227 +\item \textbf{Create a new Worksheet and initialize it to present an example from the Knowledge Base}
2.228 +\end{itemize}
2.229 +
2.230 +\subsubsection{Knowledge Browser used by the WDG}
2.231 +\begin{itemize}
2.232 +\item \textbf{Use a new or existing KB Window to browse the KB, starting at a point specified by the item highlighted in the Worksheet.}
2.233 +\end{itemize}
2.234 +
2.235 +
2.236 +\subsection{Resulting software design considerations for a worksheet component}
2.237 +
2.238 +\textbf{The contents of this section is OBSOLETE and kept temporarily for reference.}
2.239 +In this section, when IDs are mentioned, this is to be taken as a proposal.
2.240 +ID in this context means ``a way of passing access to a object''.
2.241 +Function prototypes are used as a short way of titling a paragraph, not as a definition of an interface.
2.242 +
2.243 +\subsubsection{Services/Methods offered by the worksheet component}
2.244 +
2.245 +\begin{itemize}
2.246 +\item \textbf{redisplay()} Redraws the display on demand from other components or
2.247 +the user.
2.248 +\item \textbf{update(idFormulaFrom)} Notifies the worksheet of a change in the prooftree.
2.249 +The ID of the last unchanged formula is passed. The display will be updated
2.250 +to reflect the changes. Optionally, there could be a flag passing information
2.251 +whether the calculation is still in progress or the last requested calculation
2.252 +has completed.
2.253 +\item \textbf{expand(idFormulaFrom, idFormulaTo)} (optional) Expands part of the prooftree,
2.254 +if collapsed. It is not decided yet whether other components will need a way
2.255 +of collapsing/expandig parts of the prooftree display.
2.256 +\item \textbf{collapse(idFormulaFrom, idFormulaTo)} (optional) Collapses part of the
2.257 +prooftree, if expanded. \par\centering \resizebox*{11cm}{!}{\includegraphics{fig/design_alan.eps}
2.258 +} \par{}
2.259 +\begin{figure}
2.260 +
2.261 +\caption{Environment for the worksheet component}
2.262 +\end{figure}
2.263 +
2.264 +\end{itemize}
2.265 +
2.266 +\subsubsection{Services/Methods needed by the worksheet component}
2.267 +
2.268 +Services needed for displaying the prooftree: Given a reference to a prooftree,
2.269 +the worksheet will manage its display starting from the ``top'', by asking
2.270 +(on demand) the prooftree for further elements of the tree.
2.271 +
2.272 +\begin{itemize}
2.273 +\item \textbf{idFormula getFirstFormula()} Get the ID of the first formula in the
2.274 +prooftree.
2.275 +\item \textbf{idFormula getNextFormula(idFormulaCurrent)} Get the ID of the next formula
2.276 +in the prooftree, given the current formula.
2.277 +\item \textbf{idTactic getTactic(idFormulaCurrent)} Get the ID of the next tactic
2.278 +in the prooftree, given the current formula. A special case arises if the tactic
2.279 +to continue the current calculation is solving a \textbf{subproblem}. The subproblem
2.280 +is a claculation on its own, represented by a separate proof(sub-)tree. The
2.281 +ID of the prooftree representing the subproblem is passed to the worksheet.
2.282 +The worksheet will handle the situation accordingly, e.g. by opening a new worksheet
2.283 +or displaying the (indented) new prooftree in the current worksheet.
2.284 +\end{itemize}
2.285 +Services needed for controlling the progress of calculation: The worksheet controls
2.286 +the calculation by modifying the behaviour at the hot spot in the calculation,
2.287 +the selcted active formula.
2.288 +
2.289 +\begin{itemize}
2.290 +\item \textbf{setActiveFormula(idFormula)} Makes the passed formula the active formula,
2.291 +i.e. the formula the next tactic is applied to.
2.292 +\item \textbf{indAccepted setEnteredFormula(idFormula)} Tries to replaces the active
2.293 +formula in the prooftree by the passed formula. This could fail if no valid
2.294 +derivation from the preceding formula to the (new) active formula can be found.
2.295 +\item \textbf{setNextTactic(idTactic)} Set the tactic to be used in the next step
2.296 +of calculation.
2.297 +\item \textbf{idTactic getProposedTactic()} Get the tactic proposed by the mathematics
2.298 +engine for the next step in the calculation.
2.299 +\item \textbf{listTactics getApplicableTactics()} Get a list of tactics applicable
2.300 +to the active formula.
2.301 +\item \textbf{autoCalculate(nSteps)} Calculate the next n steps starting from the
2.302 +active formula.
2.303 +\end{itemize}
2.304 +Services to handle the underlying formalization have to be discussed and added
2.305 +yet.
2.306 +
2.307 +\begin{itemize}
2.308 +\item \textbf{idFormula getFirstFormula()} Get the ID of the first formula in the
2.309 +prooftree.
2.310 +\item \textbf{idFormula getNextFormula(idFormulaCurrent)} Get the ID of the next formula
2.311 +in the prooftree, given the current formula.
2.312 +\item \textbf{idTactic getTactic(idFormulaCurrent)} Get the ID of the next tactic
2.313 +in the prooftree, given the current formula.
2.314 +\end{itemize}
2.315 +Services needed for controlling the progress of calculation: The worksheet controls
2.316 +the calculation by modifying the behaviour at the hot spot in the calculation,
2.317 +the selcted active formula.
2.318 +
2.319 +\begin{itemize}
2.320 +\item \textbf{setActiveFormula(idFormula)} Makes the passed formula the active formula,
2.321 +i.e. the formula the next tactic is applied to.
2.322 +\item \textbf{setNextTactic(idTactic)} Set the tactic to be used in the next step
2.323 +of calculation.
2.324 +\item \textbf{idTactic getProposedTactic()} Get the tactic proposed by the mathematics
2.325 +engine for the next step in the calculation.
2.326 +\item \textbf{listTactics getApplicableTactics()} Get a list of tactics applicable
2.327 +to the active formula.
2.328 +\item \textbf{autoCalculate(nSteps)} Calculate the next n steps starting from the
2.329 +active formula.
2.330 +\end{itemize}
2.331 +Services to handle the underlying formalization have to be discussed and added
2.332 +yet.
2.333 +
2.334 +%WN --- ^^^ -----------------Kopie aus UseCases am 2.9.02-----------------
2.335 +
2.336 +\subsection{Draft for an interaction diagram}
2.337 +
2.338 +\begin{itemize}
2.339 +\item they are tired and ask the system to finish the calculation (automated calculation)
2.340 +\item they know the next step and type in a tactic (input a tactic)
2.341 +\item they want to find out the next step and request a list of tactics (list of tactics)
2.342 +\item they want to find out the next step and lookup the knowledge base (look-up knowledge)
2.343 +\item they input a formula as the next step (input a formula)
2.344 +\end{itemize}
2.345 +These choices are described in the respective use cases below, where 'student' is abbreviated by S, the worksheet is abbreviated by WS, the maths engine by ME, and the dialog guide by DG.
2.346 +
2.347 +\paragraph{Automated calculation} can be requested, if the proofstate is 'safe' (indicated by ???), i.e. if the students didn't do a misleading step before in this calculation, and the system thus 'knows' how to continue.
2.348 +\begin{enumerate}
2.349 +\item S pushes a button {\it Auto} on the WS
2.350 +\item {\it Auto} sends the request {\it autoCalculate(nSteps)} to the ME %WN ODER:to the proofstate ???
2.351 +where {\it nSteps} are provided by the DG %WN(wenn vom DG, sollen wir da gleich genauer sein), oder: by the user ???
2.352 +\item the ME notifies the WS by {\it redisplay()} that the proofstate has changed
2.353 +\item the WS %WN ODER wer 'considers ...' ?
2.354 +considers the actual presentation of the proofstate (e.g. if the previously current formula is still visible), and eventually requests {\it getFromTo(currForm,Endproof)} %WN... das find ich nicht mehr, sowas \"ahnliches haben wir aber gehabt, oder ???
2.355 +from the ME
2.356 +\end{enumerate}
2.357 +
2.358 +\paragraph{Input a tactic} is possible any time in order to propagate the calculation from the current formula towards the result.
2.359 +\begin{enumerate}
2.360 +\item S inputs the tactic, where the WS distinguishes the input of a tactic - eventually containing formulas - from input of a formula belonging to the calculation
2.361 +\item the WS requests {\it setNextTactic(idTactic)} from the ME
2.362 +\item the ME notifies the WS by {\it redisplay()} that the proofstate has changed by appending (or inserting) the formula resulting from the input tactic to the proofstate
2.363 +\item the WS eventually requests {\it getFromTo(currForm,oneForm)} in order to display the resulting formula
2.364 +\end{enumerate}
2.365 +
2.366 +\paragraph{List of tactics} can be requested any time in order to receive suggestions how to proceed with the calculation. Depending on the setting of the DG, only the tactics applicable to the current formula are displayed, or some larger list.
2.367 +\begin{enumerate}
2.368 +\item S pushes a button {\it Tactics} on the worksheet
2.369 +\item the WS requests {\it getTactics(Applicable)} %WN Applicable?!
2.370 +from the ME, which returns {\it idsTactics}, a list of tactics
2.371 +\item the WS performs {\it displayTactics} %WN ???
2.372 + displaying the list in such a position on the screen, that the current formula is not covered
2.373 +\item S selects a tactic from the list, and the WS requests {\it setNextTactic(idTactic)} from the ME
2.374 +\item \dots continuation as above
2.375 +\end{enumerate}
2.376 +
2.377 +\paragraph{Look-up knowledge} is possible any time during a calculation. In general the ME may provide for special views onto the knowledge base depending on the actual proofstate. In this case the S wants to look for rules of differentiation, and we assume that there is no representation of the knowledgebase active.
2.378 +\begin{enumerate}
2.379 +\item S pushes a button {\it theories} %WN?!
2.380 +\item the WS requests {\it getCurrentTheory} %WN?!
2.381 +from the ME, which returns an {\it idTheory} %WN oder eine Liste von Theories ??? -- weiss ich selbst noch nicht genau
2.382 +\item the WS requests {\it getTheoryHierachy(idTheory)} %WN?!
2.383 +from the (???) knowledge browsers
2.384 +%WN: die Bezeichnungen 'WEB Browsers' und 'Browsers' in Andreas' Diagramm unterscheiden nicht klar genug zwischen Repr\"asentation und Steuerung; besser w\"are ???
2.385 +, which return a theory browser, with {\it idTheory} in the focus.
2.386 +\item S hits the focus, and the theory browser (???) requests {\it getTheory(idTheory)} %WN?!
2.387 +displaying the theory proposed by the ME
2.388 +\item after a while S selects the theorem {\it diff\_sum} in the theory browser, which sends the message {\it Selected(idTheorem)} to the WS
2.389 +\item the WS eventually performs {\it displayTactic} associating {\it Rewrite} and {\it diff\_sum} to the tactic {\it Rewrite diff\_sum} below the current formula
2.390 +\item {\it setNextTactic(idTactic)} as above \dots
2.391 +\end{enumerate}
2.392 +
2.393 +\paragraph{Input a formula} is interpreted as a derivation of the current formula w.r.t. the actual proofstate. The ME tries to construct this derivation (usually comprising several steps); in this case we assume that constructing the derivation is successful.
2.394 +\begin{enumerate}
2.395 +\item S inputs the formula, where the WS distinguishes the input of the formula from the input of a tactic (which may contain formulas, too)
2.396 +\item the WS requests {\it setNextFormula(idFormula)} %WN ?!
2.397 +from the ME
2.398 +\item the ME notifies the WS by {\it redisplay()} that the proofstate has changed by appending (or inserting) the formula resulting from the input tactic to the proofstate
2.399 +\item the WS eventually requests {\it getFromTo(currForm,nexEnd %WN??
2.400 +)} in order to display the resulting formula
2.401 +\end{enumerate}
2.402 +
2.403 +% WN-------------------------------------------------------------------------\\
2.404 +
2.405 +
2.406 +\subsection{}
2.407 +
2.408 +\subsection{}
2.409 +
2.410 +\subsection{}
2.411 +
2.412 +
2.413 +\section{The knowledge browsers}
2.414 +\label{SDD:knowledge_browser}
2.415 +
2.416 +%\subsection{knowledge browser}
2.417 +The knowledge browser mainly consists of three parts.
2.418 +\begin{description}
2.419 + \item [Browser-Frontend = interface to the user] Is responsible to
2.420 + answer a user request, forward it to the next layer (processor)
2.421 + encode the result in a appropriate way and return it to the
2.422 + requestor. A HTML-browser-frontend will take the requests from the
2.423 + webbrowser and return HTML-Code to the browser-window. Other
2.424 + interfaces (like a shell like one) are conceivable.
2.425 +
2.426 + \item [processor] The processor has a set of functions to gather the
2.427 + correct informations to fulfill a frontends request. e.g. if a user
2.428 + browses the knowledge-base to select a problem, the processor asks
2.429 + the dialog for a problem description and a match result and returnes
2.430 + both to the encoder.
2.431 +
2.432 + The dialog to connect to is determined by the session which is given
2.433 + by the frontend. Access permissions are controlled by dinopolis ---
2.434 + the information-processor is only allowed to connect to the dialog
2.435 + if it was allowed to in first place (on login by the session-dialog)
2.436 +
2.437 + \item [dialog] adjust a processors request to a users needs and
2.438 + permissions. Each dialog has a usermodel assigned to log his history
2.439 + and get informations about his permissions.
2.440 +\end{description}
2.441 +
2.442 +\begin{figure} [htb]
2.443 +\centerline{\psfig{figure=fig/browser_int.eps,width=11cm}}
2.444 +\caption{parts of the browser}
2.445 +\label{}
2.446 +\end{figure}
2.447 +
2.448 +The information processor can be replaced by a mock-object in the
2.449 +first development step. The ``mock information processor'' has to
2.450 +deliver example navigationtrees and the corresponding
2.451 +descriptions. So, the Information-Encoder can be developed and tested
2.452 +as disjoined Module.
2.453 +
2.454 +There is another advantage of splitting the Browser: We can excange
2.455 +the encoder part to present our information through other channels
2.456 +than HTML.
2.457 +
2.458 +\subsection{Browser Servlet}\label{SSD-browser-servelet}
2.459 + The servlet is activated whenever a User requests informations from
2.460 + the Browser. It decodes the request (URL), asks the \emph{Information
2.461 + Processor} for its infos and returns it using the \emph{Information
2.462 + Encoder} to present it.
2.463 +
2.464 + The browser-servlet is embedded within a servlet-engine
2.465 + (e.g. tomcat). The servlet-engine is working either as stand-alone
2.466 + webserver or collaborates with an running conventional web-server
2.467 + (e.g. apache). The running-mode of the servlet-engine does not affect
2.468 + the servlet - it communicates with the servlet-engine through
2.469 + well-defined interfaces. Because the running-mode depends on the
2.470 + needs of the \isac{}-host and not \isac{} itselve, the choice of its
2.471 + configuration is left to the hosts administrator.
2.472 +
2.473 + \subsubsection{request a problem-description} The request is
2.474 + recognized by the servlet-engine and forwarded to the servlet through
2.475 + its interface. Parameters contain the URL used to access the site as
2.476 + well as informations regarding the requestor. If the request occures
2.477 + the first time, the parameters have to contain a session-ID to
2.478 + determine the browser-dialog to connect to. If no session-ID is
2.479 + given, the sevlet can connect to a default browser-dialog which
2.480 + represents a ``default-user'' (or \emph{visitor}). Servlet-engines
2.481 + also support sessions to store informations about repeatedly
2.482 + connections. This feature can be used to store the dialog to
2.483 + connect. Note, that the first access has to contain the session-ID
2.484 + anyway\footnote{this can be fulfilled because the first authenticated
2.485 + access is always startet by an session-controller which first fetches
2.486 + the login-informations} and that the servlet-engines can only handle one
2.487 + session per instance of an webbrowser --- independently of the number
2.488 + of open browser-windows.
2.489 +
2.490 + The session-ID, the ID of the item to show and the presentation mode
2.491 + are used to gain the page-description from the
2.492 + information-processor. Missing informations are completed by the
2.493 + underlaying layers and does not bother the frontend. The returned
2.494 + informations can be used to generate a web-page in every case. In the
2.495 + worst case, the information-map contains a failure message to embed
2.496 + into an HTML-page.
2.497 +
2.498 + The information-encoder is used to generate a HTML-page out of the
2.499 + gained informations. Details to this process are given in section
2.500 + \ref{SDD:info_encoder}. The outcome of this method-call is the
2.501 + HTML-representation of the item to present and does not contain any
2.502 + navigational informations. The navigation tree has to be generated by
2.503 + an seperate method and is embedded when needed. The implementation
2.504 + depends of the structure of the resulting web-page. Either the
2.505 + navigation-tree is located in a seperate frame or it is delivered on
2.506 + every request. The decission is a matter of usability and should be
2.507 + left open till the usability can be tested. Therefore, content and
2.508 + navigation are built up seperatly and combined in the last step
2.509 + before deliveration to the web-browser.
2.510 +
2.511 + \subsubsection{needed methods}
2.512 +\begin{description}
2.513 + \item[String BrowserServlet.HTTP\_Request(URL)] This is a
2.514 + servlet-engine dependent method which is used by the servlet-engine
2.515 + to forward the request to the servlet\footnote{name and parameter
2.516 + might vary but the semantic of this method will be the same in all
2.517 + servlet-engines}. The URL and other context-informations (cookies
2.518 + and session-informations can be gailed from the environment) are
2.519 + used to encode the type (static, dynamic) of request and the
2.520 + information to present. This infos are used to forward the request
2.521 + to the \emph{information-processor}. The result of this request is
2.522 + combined with the navigation and returned to the servlet-engine (and
2.523 + thus to the browser-window).
2.524 +
2.525 + \item[HTMLText BrowserEncoder.encodeInformations(information\_map)]
2.526 + \ \\ see section \ref{SDD:info_encoder}
2.527 + \item[HTMLText BrowserEncoder.encodeNavigation(navigation\_map)]
2.528 + \ \\ see section \ref{SDD:info_encoder}
2.529 + \item[info\_map BProcessor.getInformation(session, descriptionID, mode)]
2.530 + \ \\ see section \ref{SDD:info_processor}
2.531 + \item[navigation\_map BProcessor.getNavigation(session, descriptionID)]
2.532 + \ \\ see section \ref{SDD:info_processor}
2.533 +\end{description}
2.534 +
2.535 +\subsection{Information encoder}
2.536 +\label{SDD:info_encoder}
2.537 +The information decoder knows about the way to present informations
2.538 +but does not have knowledge about the semantic of the
2.539 +informations. Informations are delivered inside a map. The keys are
2.540 +used to distinguish the different fields, the assigned values are then
2.541 +put into proper fields of templates. Because different kinds of
2.542 +information have to be displayed, a set of templates is used to
2.543 +generate the fitting HTML-page. Furthermore, there are some pages
2.544 +which require a strict layout rather than an automatically generated
2.545 +one (e.g. examples, example-collections). Therfore a first
2.546 +implementation might use predefined HTML-pages within the
2.547 +information-map while a more sophisticated version of the encoder
2.548 +might use a more general way to describe the layout
2.549 +(\emph{layout-hints}).
2.550 +
2.551 +Besides the pure informations regarding the displayed item, further
2.552 +information have to be encodes as there are the navigation-tree and
2.553 +meta-information which enable search-engines to recognize the
2.554 +mathematical content of the page.
2.555 +
2.556 +\subsubsection{needed methods}
2.557 +
2.558 +\begin{description}
2.559 + \item[HTMLText BrowserEncoder.encodeInformations(information\_map)]
2.560 + \ \\ encodes the given information. The generation is done with help
2.561 + of a ``template''. Basically, the template is a ready-made HTML-page
2.562 + with a few locations to fill in informations. This function has to
2.563 + parse the HTML and fill in the proper informations out of the
2.564 + information map. Different templates can be used for different
2.565 + datatypes. For instance a problem-description will have to present
2.566 + other informations than an Example or course-mainpage. Optionally, a
2.567 + predefined layout can be given within the information-map. This
2.568 + layout overrides the automatically generated one.
2.569 +
2.570 + To enhance usability of the system, some requirements regarding the
2.571 + layout have to be met:
2.572 + \begin{itemize}
2.573 +
2.574 + \item Highlite important informations: in some cases, there are
2.575 + some informations to be highlighted. e.g. if the user is forced
2.576 + to find a fitting problem for a calculation, the system can give
2.577 + feedback if the problem matches and if not it can give detailed
2.578 + informations wich requirements are not fulfilled. These
2.579 + ``matching-results'' have to be presented in a proper way.
2.580 +
2.581 + \item uniform presentation: The amount of information given
2.582 + depends on the users needs and permissions. It might be, that
2.583 + some fields available in one problem are missing in an other
2.584 + one. The encoder has to ensure, that these missing fields are
2.585 + handled in a way that the page keeps looking sound.
2.586 +
2.587 + \end{itemize}
2.588 +
2.589 + \item[HTMLText BrowserEncoder.encodeNavigation(navigation\_map)] \
2.590 + \\The navigation\_map is a hierarchical map which containes its
2.591 + nodes as labels and the next treelevel (a map of the same structure)
2.592 + as value. One node consists of the ID of an item to show and an
2.593 + ``weight'' for the order within one treelevel. The ID has to be
2.594 + translated into a link which in turn is used to load an other
2.595 + item. The structure should support expanding/collapsing of the
2.596 + branches to enhance clearness. This could be reached e.g. through
2.597 + java-script.
2.598 +
2.599 + \item[HTMLText BrowserEncoder.encodeMeta(information\_map)] \ \\
2.600 + There are several projects which try to give meta informations for
2.601 + mathematical content.\kommentar{links zu LOM, DC, MoWGLI einfuegen!}
2.602 + This method should be designed to meet the requirements of these
2.603 + projects and be flexible enough to change between them if the
2.604 + requirements change. The result of this method is put into the
2.605 + header of the result-page.
2.606 +
2.607 +\end{description}
2.608 +
2.609 +\subsection{Information processor}
2.610 +\label{SDD:info_processor}
2.611 +The information-processor is responsible for gathering the
2.612 +information. Therefore it encapsules the communication to the rest of
2.613 +the isac-system (utilizing dinopolis). It also splits the users
2.614 +request to some subrequests to the browser-dialog.
2.615 +
2.616 +The processor has an internal table to find the assigned
2.617 +browser-dialog for a session. If no reference to a dialog is present,
2.618 +the session-dialog is called to get an object-proxy of the
2.619 +browser-dialog which in turn is used to get the requested
2.620 +informations. The session-dialog (which created the browser-dialog)
2.621 +created the browser-dialog with the assigned session-ID when it
2.622 +received the request to open a new browser. (see section
2.623 +\ref{SDD:dialog})\frage{authentifikation ?}
2.624 +
2.625 +\begin{description}
2.626 + \item [InfoMap processDescription(DescriptionID, Mode)] Processes
2.627 + the informations of the wantet Description and puts it into an
2.628 + map. The resulting \emph{InfoMap} containes copies of all
2.629 + informations - changes to this Map do not affect the stored
2.630 + data. The \emph{mode} specifies the way the informations have to be
2.631 + gathered. The main types are \emph{BROWSE} and \emph{FEEDBACK} where
2.632 + FEEDBACK also has to contain the adress of the ProveState upon which
2.633 + the feedback is built.
2.634 +
2.635 + \begin{description}
2.636 +
2.637 + \item[BROWSE] the \emph{information Processor} just forwards the
2.638 + request to the \emph{DescriptionStorage} and repacks the gained
2.639 + informations.
2.640 +
2.641 + \item[FEEDBACK] the \emph{information Processor} takes the result
2.642 + from the \emph{DescriptionStorage} and overloads it with the
2.643 + informations from the ProoveState. Therefore, the ProofeState
2.644 + needs a method wich returnes how far the active information fitts
2.645 + into the State. For Example: if the displayed information is an
2.646 + Problem, the ProoveState has to perform a match between its model
2.647 + and the Problem. The result is returned to the
2.648 + \emph{informationProcessor} which fits it into the
2.649 + \emph{informationMap}. Statical informations from the
2.650 + \emph{DescriptionStorage} (where, find, \dots) are replaced by the
2.651 + state and ``comment'' of the ProveState. (e.g. ``find: x'' becomes
2.652 + ``find: item missing'')
2.653 +
2.654 + \end{description}
2.655 +
2.656 +
2.657 + \item [DescriptionObject getDescription(DescriptionID)] internal
2.658 + Method to retrieve the Description for a Problem (or Example,
2.659 + \dots). This method has to establish a connection to the
2.660 + \emph{description-storage}, encode the ID in correct manner and ask
2.661 + for the \emph{description-object}.
2.662 +\end{description}
2.663 +
2.664 +\subsection{drowser-dialog}
2.665 +
2.666 +\section{description-storage}
2.667 + When the description-storage accesses the SML-knowledge-base, there
2.668 + is an helper-layer which encodes the SML-output (text-stream) into
2.669 + JAVA-Objects and vice versa. This mechanism is not mentioned
2.670 + explicitely within this explanation.
2.671 +
2.672 +\begin{description}
2.673 + \item[MEadress getBaseRecord(Datatype)] retrieves the Base record of
2.674 + a given Datatype. For instance \emph{getBaseRecord(PROBLEM)} returns
2.675 + a adress which is understandable by the mathematic engine and points
2.676 + to the outermost Problem (e.g. [equation]). This is necessary to get
2.677 + an entry point for the further query.
2.678 +
2.679 + \item[Map getDescription(MEAdress)] retrieves the mathematical
2.680 + informations about a given entry inside the ME. The Map consists of
2.681 + the field identifyer (as used within SML) and the assigned data. The
2.682 + datatype suits the SML-datatype but is delivered as JAVA-Object
2.683 + (e.g. a SML-List is encoded to a JAVA-List). Among others, the Map
2.684 + containes ``children'' which contain a list like [[equation,
2.685 + univariate, linear], [equation, univariate, plain\_square],
2.686 + [equation, univariate, polynomial], \dots]
2.687 +
2.688 + \item[DescriptionID storeDescription(Map)] takes the information as
2.689 + given by the ME and stores it inside a database. Therefore it is
2.690 + neccessary to convert it into fitting Datatypes understood by the
2.691 + Database.
2.692 +
2.693 + \item[void fetchData(Datatype)] fetches the BaseRecord of the
2.694 + Datatype (e.g. PROBLEM) and uses \emph{getDescription} to traverse
2.695 + recursively through the whole Datastructure to generate the
2.696 + information of the whole information-tree.
2.697 +
2.698 + \item[DescriptionObject getDescription(DescriptionID)] returnes the
2.699 + \emph{description-object} which handles the given description. If
2.700 + this method is called twice targeting the same description, one and
2.701 + the same \emph{description-object} is returned.
2.702 +
2.703 + \item[DescriptionID createDescription(Datatype)] creates a new
2.704 + Description of the given Type and return its ID. The Datatype
2.705 + identifies the number, type and names of fields which are mandatory
2.706 + and optional for the record\footnote{The datatype might be specified
2.707 + in a DLD and has to contain metadata as: is the data stored inside
2.708 + the ME, which fields are only to be changed by the ME, which
2.709 + identifyer has the Datatype within the ME, \dots}.
2.710 +
2.711 + \item[List queryDescriptions(criteria)] queries the database for
2.712 + Descriptions matching the given criteria. This criteria can be
2.713 + e.g. Datatype, modification Date, parts of the name, \dots. The
2.714 + identifyers of the matching Descriptions are returned to the caller.
2.715 +
2.716 + \item[navigationTree getNavigation(navId)] builds and returns a
2.717 + structure which describes a navigation Tree. navigationTree is a
2.718 + ``nested Map''-like structure but with an unique order of its
2.719 + keys. \\ A key represents a node inside the tree and contains name
2.720 + and reference of the related content - the assigned value is a
2.721 + structure of the same type or \emph{null}. So, the full tree is
2.722 + recursively built.
2.723 +
2.724 + \item[navId newNavigation(navigationTree)] store a new navigationTree
2.725 + in the description-store.
2.726 +
2.727 + \item[List queryNavigation(Criteria)] query the description-store for
2.728 + a list of Navigation Trees. Criteria can contain Informations like
2.729 + the content of the tree (e.g. differential equation).
2.730 +
2.731 + %\item[set navigation] ??? immuteable navigationtrees ? wenn ein tree
2.732 + %geaendert wird, muss er neu gesetzt werden ?
2.733 +
2.734 +\end{description}
2.735 +
2.736 +\subsection{description-object}
2.737 +\begin{description}
2.738 + \item[Map getFields()] Returnes a Map of the contained fields and
2.739 + their types (Maps fieldnames to a fielddescription: datatype,
2.740 + optional)
2.741 +
2.742 + \item[Object getField(fieldname)] Returnes the assigned Field. The
2.743 + returned values has to be immutable as a datachange is only allowed
2.744 + through the respective set-Method.
2.745 +
2.746 + \item[boolean setField(fieldname, value)] sets the field
2.747 + \emph{fieldname} to \emph{value}. This operation might fail if the
2.748 + user does not have the permission to change the field, or
2.749 + \emph{value} is of the wrong type.
2.750 +
2.751 + \item[boolean getWritelock()] request a writelock
2.752 +
2.753 + \item[void releaseWritelock()] release the writelock to let other
2.754 + users change the description
2.755 +
2.756 + \item[DescriptionID createChild()] create a new Child of the same
2.757 + Datatype for this description. This is useful for Examples but not
2.758 + possible for all types of descriptions. e.g. The children of a
2.759 + Problem are only created out of the ME - it is not possible for a
2.760 + user to create a new Problem!
2.761 +
2.762 +\end{description}
2.763 +
2.764 +\section{The Dialog}
2.765 +\label{SDD:dialog}
2.766 +The dialog represents the \isac{}-layer which connects the
2.767 +frontend-applications with the backend-ressources (math-engine,
2.768 +description-storage, \dots). It is responsible to adjust the behaviour
2.769 +of the system to the users needs and permissions. (see \ref{ADD:dialog})
2.770 +
2.771 +The ``heart'' of the dialog-layer is the \emph{session-dialog}. It
2.772 +instantiates new sessions and browser-- or worksheet-- dialoges when
2.773 +needed. It also registers them on the security system to grant
2.774 +access-permissions as needed. Therefore, the session-dialog has to be
2.775 +instantiated on system-startup and registered an the
2.776 +\emph{dinopolis}\/-NameService to be found by the frontend-applications.
2.777 +
2.778 +\subsection{create a new session}
2.779 +A new session is initiated by the session-controller. This is a
2.780 +client-side java-programm which queries the dinopolis-nameservice for
2.781 +the session-dialog and connects with it. The session-dialog requires a
2.782 +username and the assigned passwort. If the user is assigned to more
2.783 +then one user-group, it is necessary to enter the active group for the
2.784 +session (the group determines the behaviour of \isac). The
2.785 +session-dialog prepares the user-model for the user and returns
2.786 +user-preferences to the session-controller if wanted.
2.787 +
2.788 +\subsubsection{needed methods}
2.789 +\begin{description}
2.790 + \item[groupset SessionDialog.login(username, password)] A public
2.791 + method to performs an user-login to \isac. If username and password
2.792 + fit, the set of possible groups for the user are returned to the
2.793 + caller and the caller is registered on the dinopolis-securityManager
2.794 + to be autorized to connect to the private methods (openSession)
2.795 + \frage{laesst sich der caller mit dino-mitteln
2.796 + feststellen?}. Otherwise \emph{null} is returned to inform the
2.797 + caller that the login was not successful.
2.798 +
2.799 + \item[boolean SessionDialog.openSession(group)] This method is only
2.800 + accessible for authenticated DinoObjects which performed a login
2.801 + previousely. If the group fits the assigned user, a new session is
2.802 + created and assigned to the gid of the caller\footnote{Usually, the
2.803 + caller will be of type \emph{SessionController}}
2.804 +
2.805 + \item[Map SessionDialog.getUserPreferences()] This method is only
2.806 + accessible for authenticated DinoObjects which performed a login
2.807 + previousely. A set of readable preferences (such as a
2.808 + ``default-group'') is returned. Note that there are preferences
2.809 + which might be readable but not writeable and others which are not
2.810 + even readable and therefore not included in the returnvalue of this
2.811 + method.
2.812 +
2.813 + \item[boolean SessionDialog.setUserPreferences()] This method is only
2.814 + accessible for authenticated DinoObjects which performed a login
2.815 + previously. It is used to alter a users preferences. The
2.816 + session-dialog checks if all contained preferences are writeable for
2.817 + the user before it trys to write them to the user-model.
2.818 +
2.819 +\end{description}
2.820 +
2.821 +\subsection{open a new browser (--window)}
2.822 +Anthough the WebBrowser runs on the client-side and connects to an
2.823 +already running WebServer (see Section \ref{SDD:knowledge_browser}),
2.824 +interaction with the session-dialog is necessary to prepare the system
2.825 +for the request. The request to open a new browser-window can result
2.826 +either from the user himself (through the session-controller) or from
2.827 +an other part of the dialog (worksheet-dialog if the user is forced to
2.828 +search an item by himselve or browser-dialog if the user jumps into an
2.829 +other part if the knowledge).
2.830 +
2.831 +For the session-dialog, it does not matter who opens the new
2.832 +browser-window - the behaviour is always the same (access-control is
2.833 +done through dinopolis)
2.834 +
2.835 +\subsubsection{needed methods}
2.836 +\begin{description}
2.837 + \item[boolean SessionDialog.openBrowser(params)] This method is only
2.838 + accessible, if the caller is explicitely allowed to
2.839 + connect\footnote{the session-dialog gave the permission before
2.840 + e.g. while login or because the caller was created by the
2.841 + session-dialog}. The session-dialog looks for the
2.842 + \emph{browser-dialog} which handles the knowledge-access for the
2.843 + current session. If no browser-dialog was found, a new one is
2.844 + created and registered to be allowed to access the current
2.845 + sessiondialog.
2.846 +
2.847 + \emph{params} contains information as start-point and mode of the
2.848 + access (e.g. problem to start the search from, mode:dynamic to tell
2.849 + the browser to present the match-results, id of the calculation
2.850 + within the worksheet-dialog to match with).
2.851 +
2.852 + Depending on the type of browser to use (stored in the preferences),
2.853 + this informations are encoded to an program-call and passed to the
2.854 + session-controller which executes it. (in case of the http-accessed
2.855 + browser this programm call could look like ``mozilla -remote
2.856 + http://knowledge.isac.at//\-sid=12345\&type=passive'')
2.857 +
2.858 + \item[SessionController.execute(Object programmCall)] Executes the
2.859 + given program. \emph{programCall} can also contain information if
2.860 + the program to call is native or a java-program (the later can be
2.861 + called within the same java-machine)\footnote{for informations
2.862 + regarding the execution of the browser-call see section
2.863 + \ref{SDD:knowledge_browser}}
2.864 +
2.865 +% This informations are
2.866 +% passed to the browser-dialog to prepare it for the upcomming
2.867 +% request. The browser-dialog stores the informations and returns an
2.868 +% id
2.869 +
2.870 +\end{description}
2.871 +
2.872 +\subsection{open a new worksheet}
2.873 +Opening a new worksheet is similar than open open a new
2.874 +browserwindow. Additional to the single programcall, a new ProoveState
2.875 +has to be instantiated and filled with the correct informations. The
2.876 +request to open a new worksheet can result either from the user
2.877 +himselve or from an other part of the dialog (the browser can start
2.878 +the calculation of an example or start an empty
2.879 +calculation). Therefore the browser (-dialog) has to instantiate a new
2.880 +provestate and fill in the informations used to start the calculation
2.881 +(see Section \ref{SDD:knowledge_browser} for details) Afterwards, the
2.882 +provestate is given to the worksheet-dialog to enable the worksheet to
2.883 +continue the calculation.
2.884 +
2.885 +\subsubsection{needed methods}
2.886 +\begin{description}
2.887 + \item[boolean BrowserDialog.openWorksheet(params)] If the Browser is
2.888 + used to initiate a new worksheet, this method is called from the
2.889 + processor to initiate the ProofState and forward the request to the
2.890 + session-dialog. The \emph{params} contain the id of the example to
2.891 + calculate if any. First, the BrowserDialog has to connect the
2.892 + Description-Storage to gather the informations of the example. Then,
2.893 + the new ProofState is instantiated and filled with the data. This
2.894 + ProofState is used to call the SessionDialog which instantiates a
2.895 + new WorkSheet and connects it with the ProofState (through the
2.896 + worksheet-dialog).
2.897 +
2.898 + \item[boolean SessionDialog.openWorksheet(ProofState)] This method
2.899 + is only accessible, if the caller is explicitely allowed to
2.900 + connect. The \emph{ProofState} already containes all information
2.901 + which are needed to for the calculation. The session-dialog connects
2.902 + the responsible worksheet-dialog (or instantiates a new one if no is
2.903 + running) and passes the proof-state. The return-value containes an
2.904 + identifyer of the running calculation. The SessionController is
2.905 + called with this id to start a new worksheet. The new worksheet uses
2.906 + this number to establish an connection to its dialog. Any further
2.907 + communication bypasses the session-dialog.
2.908 +
2.909 +
2.910 +
2.911 +\end{description}
2.912 +
2.913 +\section{The browser generators}
2.914 +create a XML-description out of the knowledge-database.
2.915 +\subsection{}
2.916 +
2.917 +\subsection{}
2.918 +
2.919 +\subsection{}
2.920 +
2.921 +\subsection{}
2.922 +
2.923 +\subsection{}
2.924 +
2.925 +
2.926 +\section{The example browser and generator}
2.927 +
2.928 +%\subsection{}
2.929 +
2.930 +%\subsection{}
2.931 +
2.932 +%\subsection{}
2.933 +
2.934 +
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc/sdd.tex Thu Apr 17 18:01:02 2003 +0200
3.3 @@ -0,0 +1,41 @@
3.4 +%\date{$Revision$}
3.5 +\documentclass[a4wide]{report}
3.6 +\usepackage{epsfig}
3.7 +\usepackage{latexsym}
3.8 +\bibliographystyle{alpha}
3.9 +
3.10 +\newcommand {\kommentar}[1]{\marginpar{\begin{flushright}\tiny#1\end{flushright}}}
3.11 +\newcommand {\frage}[1]{
3.12 + \marginpar{
3.13 + \begin{tabular}{p{5mm} p{2cm}}
3.14 + \begin{flushleft}
3.15 + {\large?}
3.16 + \end{flushleft}
3.17 + &
3.18 + \begin{flushright}
3.19 + \tiny #1
3.20 + \end{flushright}
3.21 + \\
3.22 + \end{tabular}
3.23 + }
3.24 +
3.25 + }
3.26 +\newcommand {\bigquest}{\marginpar{\huge?}}
3.27 +
3.28 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
3.29 +\def\sisac{{\small${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
3.30 +
3.31 +\title{\isac\\ Software Design Document}
3.32 +\author{Andreas Griesmayer, Alan Krempler, Walther Neuper\\
3.33 +{\tt\{agries,akremp,neuper\}@ist.tugraz.at}}
3.34 +\date{$Revision$}
3.35 +%AG2.1.03 Dialog Layer
3.36 +
3.37 +\includeonly{sdd-content}
3.38 +\begin{document}
3.39 +\maketitle
3.40 +\tableofcontents
3.41 +
3.42 +\input{common}
3.43 +\bibliography{bib/didact,bib/math-eng,bib/dia-form,bib/RISC_1,bib/RISC_2,bib/misc,bib/hci,bib/isac}
3.44 +\end{document}
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc/srd-content.tex Thu Apr 17 18:01:02 2003 +0200
4.3 @@ -0,0 +1,291 @@
4.4 +%nicht vergessen: auch srd.tex ($Revision $) \"andern !
4.5 +\chapter{Software Requirements Document}
4.6 +
4.7 +This Software Requirements Document is structured along the modules
4.8 +abstracted from the functionality defined in the User Requirements
4.9 +Document. The User Requirements Document, however, is structured along
4.10 +the different kinds of users envisaged. In order to establish
4.11 +comfortable tracing, the $m:n$ relation between user requirements and
4.12 +software requirements will be accurrately recorded in a double-linked
4.13 +way.
4.14 +
4.15 +\section{General requirements}
4.16 +%One goal of this section is to achieve a smooth design and minimize the effort in development. Although \sisac consists of a number of (more or less) autonomous modules, a number of developments can be shared.
4.17 +
4.18 +\subparagraph{Delopment environment,} standards and components, documentation and revision control are described in appendix \ref{AP:environment}.
4.19 +
4.20 +\subparagraph{The call hierarchy} between the components underlies a severe restriction due to UR \ref{access-ab} and UR \ref{isac-www}: Because a browser can only deliver a HTTP-request, the worksheet must start browsers, too (and not only the dialog, as it would be desirable w.r.t. the system architecture).
4.21 +{\bf\SR Browsers are called by a 'master-browser' {\em and} by the worksheet. \label{}} ??? %WN2.12.02 ...... ausbessern !!!!
4.22 +
4.23 +\subparagraph{The connection between Java and SML} has to be 'hand-made'. During the next few years there will be several changes at the interfaces between the
4.24 + \sisac-components belonging to these two language environments.
4.25 +{\bf\SR The SML-kernel is started by a java thread \label{}} which controls the time-out eventuall resulting from non-terminating loops in the knowledge interpreter.
4.26 +{\bf\SR The SML standard-output channel is read by parsers, \label{}} one for the SML-structures, and one for the mathematics formulas embedded in the SML-structures.
4.27 +
4.28 +\subparagraph{System requirements for the users:} Users (with exception of the math authors, which work directly on the SML-kernel) are expected to work on standard-browsers (UR \ref{browser}) and some additional software components.
4.29 +{\bf\SR On the client-side a Java virtual machine version .... \label{}} must reside on the local computer of the learners and authors.
4.30 +{\bf\SR On the server there is a Linux or Unix \label{}} operating system, Linux version ..., Unix ...
4.31 +
4.32 +
4.33 +
4.34 +\section{The worksheet}
4.35 +A worksheet is the protocol of a more or less interactive calculation of an example, and it offers access to all services necessary to calculate the result of the example.
4.36 +
4.37 +\subparagraph{A calculation mirrors the structure of the prooftree.}
4.38 +{\bf\SR The structure of a calculation is given by the ME. \label{}} Consequently any editing in a calculation affects the parts depending on the edited formula or tactic. Edit the worksheet w.r.t. UR \ref{edit} for publication etc. is done outside \sisac{} after having exported the calculation.
4.39 +{\bf\SR Export a calculation to a standard format \label{}} preferably XML plus MathML.
4.40 +
4.41 +%{\bf\SR \label{}}
4.42 +
4.43 +
4.44 +\section{The browser generators}
4.45 + \sisac's mathematics knowledge (on (1)theories (2)problems (3)methods)
4.46 + is held in SML datastructures. Here we describe all requirements
4.47 + concerning the generation of the browsers written in Java, whereas
4.48 + the generation of the math knowledge itself is described in the
4.49 + 'interfaces for authors of math knowledge'.
4.50 +
4.51 +The browser generators provide the contents for the browsers. This
4.52 +means that a browser querys its respective browser generator about
4.53 +subnodes etc. whereas the further description is held outside the
4.54 +SML-engine. To maintain this connection, unique identifyer are needed.
4.55 +{\bf\SR browser-generators use locally unique identifyers \label{}} (locally unique within SML) for their informations (for each node of their structure).
4.56 +
4.57 +\subparagraph{Data are structured hierarchically,} i.e. the problems, methods and examples. (The theories for a directed graph without cycles; thus it also can presented by a hierarchy.)
4.58 +{\bf\SR The hiearchy displayed in a frame \label{}} in order to have it visible all the time.
4.59 +{\bf\SR The hierarchy has arbitrary levels. \label{}} For the headlines for each level see SR \dots SR \ref{expl-headlines}.
4.60 +{\bf\SR The hierarchy shows the position \label{}} of the related element displayed in the browser-window; for this purpose an additional button is required, because the 'back' and 'forward'-button on the browser may disconnect the relation.
4.61 +
4.62 +
4.63 +\subsection{The theory browser generator}
4.64 +The generation of the theory browser is already implemented by Isabelle. Within phase 1 of development, \sisac{} will take this component without any change.
4.65 +{\bf\SR The theory browser generator is given by Isabelle. \label{gen-isa}}
4.66 +
4.67 +\subsection{The problem and method browser generators}
4.68 +.
4.69 +
4.70 +\subsection{The example browser generator}
4.71 +This authoring component comprises all tools necessary to generate the content displayed by the example browser.
4.72 +
4.73 +{\bf\SR The headlines of the example-hierarchy: \label{expl-headlines}} The hierarchy comprises the labels of the chapters, sections, subsections etc. plus the respective head line, and the blocks of examples with the respective labels -- all defined by the user (see UR \ref{UR161a}).
4.74 +
4.75 +{\bf\SR Integrated editors for text, formulas and figures. \label{}} This integration should be as smooth as possible; it includes an MathML-based formula-editor for the formalization.
4.76 +
4.77 +\section{The knowledge browsers}
4.78 +\label{kbrowser}
4.79 +%W.N.: dieser Abschnitt ist f''ur A.G. + W.N.
4.80 +All browsers (Example-Browser and Knowledge-Browsers) present their
4.81 +output in a similar way. Textual descriptions have to be combined with
4.82 +images, formulas, formalisations, problems, \dots and links to further
4.83 +informations(UR\ref{URinterlink}). The structure of this informations
4.84 +has to be taken from the respective browser-generators. All kinds of
4.85 +information might be interlinked among each other, but not all parts
4.86 +of the information might be already present in the system when a new
4.87 +item is inserted. (e.g. a example might use the keyword
4.88 +\emph{is\_rooteq\_in} in its \emph{where}\/clause before the keyword
4.89 +is described in the system. If the example is viewed after a
4.90 +description became available, a link to the explanation should be
4.91 +provided automatically.) To support this feature, the browsers need a
4.92 +fast way to look up a special description.
4.93 +{\bf\SR fast look up for description (includes resolve of the
4.94 +identifyer and query for a description)}
4.95 +
4.96 +\subparagraph{Groups of users} are usually 1-to-1 related to courses; members of courses get specific examples and specific advice by explanations.
4.97 +{\bf\SR Each user is assigned exactly one group during a session. \label{}} The user, however, may start another session as a member of another group.
4.98 +{\bf\SR There is a default group for visitors. \label{}}
4.99 +{\bf\SR \label{}}
4.100 +
4.101 +\subparagraph{Additional data and visibility properties:} A considerable part of the data are additional to the data generated from the SML structures. The visibility concerns enabled or disabled links from problem and methods, and the access to examples from the hierarchy frame. There are respective time constraints on the visibility.
4.102 +{\bf\SR Additional data and visibility are course specific. \label{}}
4.103 +{\bf\SR Time constraints are given by intervals; \label{}} there are specific values for the limits of the interval indicanting infinity (contraint is given from the very beginning, or lasts forever).
4.104 +
4.105 +
4.106 +\subsection{The theory browser}
4.107 +The theory browser is already implemented by Isabelle. Within phase 1 of development, \sisac{} will take this component without any change.
4.108 +{\bf\SR the theory browser is given by Isabelle. \label{}}
4.109 +
4.110 +\subsection{The problem and method browsers}
4.111 +%\subparagraph{Static and dynamic views onto the KB} are provided by both browsers. Thus the (HTML-) presentation is generated dynamically. The dynamic view for problemjs concerns instantiation by a model of the current calculation on the worksheet. The dynamic view for methods concerns marking the tactic currently applied in a calculation.
4.112 +%{\bf\SR Browsers create the presentation in browser-windows dynamically. \label{}}
4.113 +
4.114 +\subparagraph{Additional data} are explanations and typical examples which may be provided for each problem and each method. Both of these kinds of additional data are spcific for courses and may underly time constraints (UR \ref{expl-locked}, UR \ref{invisible}, UR \ref{restrict-know}).
4.115 +
4.116 +The primary contents are the respective problem and the respective method; {\em all} other data are reachable by links. This holds for special mathematical data (on rulesets etc.) from SML, too.
4.117 +{\bf\SR A problem-page consists of \label{problem-page}} the
4.118 +\begin{tabbing}
4.119 +12345\=123\=123\=\kill
4.120 +\>name of the problem\\
4.121 +\>the fields 'given', 'where', 'find' and 'relate'\\
4.122 +\>a link to the special math data\\
4.123 +\>a list of subordinated methods (only displayed in the hierarchy-frame)\\
4.124 +\>an arbitrary list of links to additional data
4.125 +\end{tabbing}
4.126 +The next lower and next higher level in the hierarchy can be found in the hierarchy-frame.
4.127 +{\bf\SR A method-page consists of \label{method-page}}
4.128 +\begin{tabbing}
4.129 +12345\=123\=123\=\kill
4.130 +\>name of the method\\
4.131 +\>the script\\
4.132 +\>a link to the special math data\\
4.133 +\>a list of subordinated methods (only displayed in the hierarchy-frame)\\
4.134 +\>an arbitrary list of links to additional data
4.135 +\end{tabbing}
4.136 +{\bf\SR The links to additional data \label{}} have the following attributes:
4.137 +\begin{tabbing}
4.138 +12345\=123\=123\=\kill
4.139 +\>text on the link\\
4.140 +\>the reference (to an explanation or to an example starting a worksheet)\\
4.141 +\>groups\\
4.142 +\>\>ID of first group\\
4.143 +\>\>\>locked: list of intervals\\
4.144 +\>\>\>???used by userID ---$>$ usermodel???\\
4.145 +\>\>ID of second group \dots
4.146 +\end{tabbing}
4.147 +%{\bf\SR Explanations and examples are optional. \label{}} For each problem and each method there is {\em one ???} link for the explanations and {\em one} link for the examples (which may be disabled).
4.148 +%{\bf\SR Access to explanations and examples of other courses \label{}} is possible by ... ??? (see UR \ref{other-courses}).
4.149 +
4.150 +
4.151 +
4.152 +
4.153 +\subsection{The example browser}
4.154 +In contrary to the problem and method browsers, the presentation of the contents of a browser-window is {\em not} generated automatically. UR \ref{expl-layout} requests for a layout 'handmade' by the course designer; there are, however, a lot of attributes invisible for the learner to be added by the course designer, too.
4.155 +
4.156 +\subparagraph{Attributes of examples and collections} are numerous, and thus defaults help to safe space. There is only one collection, partitioned hierarchically into subcollections.
4.157 +{\bf\SR Default data \label{}} are filled in bottum up: A default is filled by the first non-default parent.
4.158 +{\bf\SR A subcollection has the attributes \label{coll-attr}}
4.159 +\begin{tabbing}
4.160 +12345\=123\=123\=123\=123\=\kill
4.161 +\>headline of the collection (displayed also in the hiearchy-frame) \\
4.162 +\>description of the collection\\
4.163 +\>list of subcollections\\
4.164 +\>OR\\
4.165 +\>layout of examples belonging to this subcollection\\
4.166 +\>author\\
4.167 +\>copyright owner\\
4.168 +\>groups of users, for each group: \\
4.169 +\>\>ID of the group \\
4.170 +\>\>schemas \\
4.171 +\>\>\>error \\
4.172 +\>\>\>fill-in \\
4.173 +\>\>\> \\
4.174 +\>\>dialog \\
4.175 +\>\>\>blackbox \\
4.176 +\>\>\>detail \\
4.177 +\>\>\>activity \\
4.178 +\>\>\>stepwidt \\
4.179 +\>\>\> \\
4.180 +\>\>invisible: list of intervals OR duration (? TODO !)\\
4.181 +\>\>locked: list of intervalsOR duration (? TODO !) \\
4.182 +\>\>evaluation \\
4.183 +\>\>\>TODO: difficulty, length, \dots \\
4.184 +\>\>\>finished-by: \\
4.185 +\>\>\>\>elements: list of mandatory examples (or groups) to be done \\
4.186 +\>\>\>\>number: number of (arbitrary) examples (or groups) to be done \\
4.187 +\>\>\>\>points: calculated from TODO: difficulty, length, \dots \\
4.188 +\end{tabbing}
4.189 +Pay attention to the entry 'list of subcollections OR ayout of examples belonging to this subcollection': This means that the subcollection {\em exactly one} hierarchy-level above the bottom of individual examples has a specific content, the graphical layout of the examples. This is in order to meet UR \ref{expl-layout}.
4.190 +
4.191 +
4.192 +{\bf\SR An example has the attributes \label{expl-att}}
4.193 +\begin{tabbing}
4.194 +12345\=123\=123\=123\=123\=123\=\kill
4.195 +\>label \\
4.196 +\>reference ??? to the description of the example (in the layout ?)\\
4.197 +\>list of formalizations and specifications \\
4.198 +\>author\\
4.199 +\>copyright owner\\
4.200 +\>time stamp\\
4.201 +\>groups of users, for each group: \\
4.202 +\>\>ID of the group \\
4.203 +\>\>schemas \\
4.204 +\>\>\>error \\
4.205 +\>\>\>fill-in \\
4.206 +\>\>\> \\
4.207 +\>\>dialog \\
4.208 +\>\>\>blackbox \\
4.209 +\>\>\>detail \\
4.210 +\>\>\>activity \\
4.211 +\>\>\>stepwidt \\
4.212 +\>\>\> \\
4.213 +\>\>invisible: list of intervals OR duration (? TODO !) \\
4.214 +\>\>locked: list of intervals OR duration (? TODO !)\\
4.215 +\>\>evaluation \\
4.216 +\>\>\>TODO: difficulty, length, \dots \\
4.217 +\>\>???done by userID ---$>$ usermodel???
4.218 +\end{tabbing}
4.219 +{\bf\SR Hitting the label of the example starts the calculation. \label{}}
4.220 +
4.221 +\subparagraph{Visibility of the examples} is defined in two levels: (1) 'locked' displays the text of the example, but doesn't allow to calculate it; and (2) 'invisible' desn't display the example at all.
4.222 +{\bf\SR {\em Only} visible examples are checked for being locked.\label{}}
4.223 +%{\bf\SR Authoring-/learner-mode:} the formalization and other attributes are shown/not shown, depending on the group the user belongs to.
4.224 +
4.225 +%\subparagraph{}
4.226 +%{\bf\SR \label{}}
4.227 +
4.228 +
4.229 +
4.230 +\section{The dialog guide}
4.231 +
4.232 +%{\bf\SR A learner has a dialog state within the current session. \label{}}
4.233 +%{\bf\SR Each learner has a history of all sessions. \label{}}
4.234 +%{\bf\SR The history holds the condensed performance in calculations. \label{}}
4.235 +%{\bf\SR The history holds requests into the knowledge. \label{}\\}
4.236 +%\subparagraph{}
4.237 +%{\bf\SR \\}
4.238 +
4.239 +As already mentioned, the dialog guide will be fleshed out in a later phase of development involving didactics and learning theory. Now we try to establish a framework open for later completion.
4.240 +
4.241 +\subparagraph{The dialogstate} is read and updated during {\em one} session. A dialog resumes the dialogstate from the previous session done as a member of the same student-group.
4.242 +{\bf\SR The last dialog is stored \label{}} for each group the student is a member of. When storing and replacing the previous dialogstate, this dialogstate is transferred to the history of the usermodel (eventually after compression).
4.243 +{\bf\SR The dialogstate has the attributes \label{}}
4.244 +{\small
4.245 +\begin{tabbing}
4.246 +12345\=123\=123\=123\=123\=123\=123\=123\=12345123\=123\=\kill
4.247 +\>begin \>\>\>\>\>\>\>\>\>timestamp of begin of session\\
4.248 +\>provided-end\>\>\>\>\>\>\>\>\>e.g. for examinations\\
4.249 +\>actual-end \>\>\>\>\>\>\>\>\>empty, or timestamp of end of session\\
4.250 +\>group \>\>\>\>\>\>\>\>\>the user has started the session with\\
4.251 +\>interactions, for each: \\
4.252 +\>\>timestamp\\
4.253 +\>\>label of example\>\>\>\>\>\>\>\>empty if \sisac{} entered via KB\\
4.254 +\>\>input\>\>\>\>\>\>\>\>tactic, formula, command or label in KB\\
4.255 +\>\>response\>\>\>\>\>\>\>\>??? of which part of system ???\\
4.256 +\>\>pattern\>\>\>\>\>\>\>\>of dialog\\
4.257 +\>\>\>activity\\
4.258 +\>\>\>stepwidt\\
4.259 +\>\>\>\dots TODO \dots\\
4.260 +\end{tabbing}}
4.261 +The use of these fields is shown by use-case UC TODO.
4.262 +
4.263 +
4.264 +\subparagraph{The usermodel} consists of two parts: the settings of the personal preferences and the history of (condensed) dialogstates. The history is constructed from the dialogstates: before a dialogstate is being replaced at the start of a new session, its data are restructured and appended to the history.
4.265 +{\bf\SR The usermodel has the attributes\label{}}
4.266 +{\small
4.267 +\begin{tabbing}
4.268 +12345\=123\=123\=123\=123\=123\=123\=123\=12345123\=123\=\kill
4.269 +\>settings\\
4.270 +\>\>patterns, for each:\>\>\>\>\>\>\>\>of dialog\\
4.271 +\>\>\>activity\\
4.272 +\>\>\>stepwidt\\
4.273 +\>\>\>\dots TODO \dots\\
4.274 +\>history, for each session:\>\>\>\>\>\>\>\>\>\\
4.275 +\>\>begin\_end\>\>\>\>\>\>\>\>2 timestamps\\
4.276 +\>\>group\>\>\>\>\>\>\>\> the user has started the session with\\
4.277 +\>\>kb\_touchs, for each:\>\>\>\>\>\>\>\>\\
4.278 +\>\>\>label of KB item\\
4.279 +\>\>\>timestamps\\
4.280 +\>\>examples, for each:\\
4.281 +\>\>\>label of example\\
4.282 +\>\>\>begin\_end\>\>\>\>\>\>\>2 timestamps\\
4.283 +\>\>\>finished\>\>\>\>\>\>\>yes/no\\
4.284 +\>\>\>performance\>\>\>\>\>\>\>from example.evaluation.TODO and\\
4.285 +\>\>\>\>\>\>\>\>\>\>from dialog.interactions\\
4.286 +\end{tabbing}}
4.287 +The use of these fields is shown by use-case UC TODO.
4.288 +
4.289 +
4.290 +\section{The mathematics engine}
4.291 +Here only these requirements are recorded which have been newly raised when specifying the interfaces to the ME.
4.292 +
4.293 +{\bf\SR The structure of a calculation is given by ??? for each formula\label{}}
4.294 +