wneuper/isa: comparison doc-src/isac/jrocnik/eJMT-paper/jrocnik

equal deleted inserted replaced

-:b18ff622ad05
+:7132779e2ff4
 specific services. An important part of such services is called
 ``next-step-guidance'', generated by a specific kind of ``TP-based
 programming language''. In the
 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
 a language is prototyped in line with~\cite{plmms10} and built upon
-the theorem prover.
+the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}
-Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
+\footnote{http://isabelle.in.tum.de/}.
 The TP services are coordinated by a specific interpreter for the
 programming language, called
 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the
 interpreter will be briefly re-introduced in order to make the paper
 self-contained.
 in a case study by the author. The author was considered an ideal
 candidate for this study for the following reasons: as a student in
 Telematics (computer science with focus on Signal Processing) he had
 general knowledge in programming as well as specific domain knowledge
 in Signal Processing; and he was {\em not} involved in the development of
-{\sisac}'s programming language and interpreter, thus a novice to the
+{\sisac}'s programming language and interpreter, thus being a novice to the
 language.
-The goal of the case study was (1) some TP-based programs for
+The goals of the case study were: (1) to identify some TP-based programs for
 interactive course material for a specific ``Advanced Signal
 Processing Lab'' in a higher semester, (2) respective program
-development with as little advice from the {\sisac}-team and (3) records
+development with as little advice as possible from the {\sisac}-team and (3)
-and comments for the main steps of development in an Isabelle theory;
+to document records and comments for the main steps of development in an
-this theory should provide guidelines for future programmers. An
+Isabelle theory; this theory should provide guidelines for future programmers.
-excerpt from this theory is the main part of this paper.
+An excerpt from this theory is the main part of this paper.
 \par
 The paper will use the problem in Fig.\ref{fig-interactive} as a
 running example:
 \begin{figure} [htb]
 \begin{center}
 dialogue authors (in Java-based tools), using TP services provided by
 Lucas-Interpretation. The latter acts on programs developed by
 mathematics-authors (in Isabelle/ML); their task is concern of this
 paper.
-\paragraph{The paper is structured} as follows: The introduction
+The paper is structured as follows: The introduction
 \S\ref{intro} is followed by a brief re-introduction of the TP-based
 programming language in \S\ref{PL}, which extends the executable
 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
 play a specific role in Lucas-Interpretation and in providing the TP
 services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes
 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
 The executable fragment consists of data-type and function
 definitions.  It's usability even suggests that fragment for
-introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
+introductory courses \cite{nipkow-prog-prove}. HOL (Higher-Order Logic)
-whose type system resembles that of functional programming
+is a typed logic whose type system resembles that of functional programming
 languages. Thus there are
 \begin{description}
 \item[base types,] in particular \textit{bool}, the type of truth
 values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
 natural, integer and complex numbers respectively in mathematics.
 \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
 \;)$.
 \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
 The prototype extends Isabelle's language by specific statements
-called tactics~\footnote{{\sisac}'s tactics are different from
+called tactics~\footnote{{\sisac}'s. This tactics are different from
 Isabelle's tactics: the former concern steps in a calculation, the
 latter concern proofs.}  and tactics. For the programmer these
 statements are functions with the following signatures:
 \begin{description}
 07         else NONE
 08     | eval_argument_in _ _ _ _ = NONE;
 09   *}
 \end{verbatim}}
-\noindent The function body creates either creates \texttt{NONE}
+\noindent The function body creates either \texttt{NONE}
 telling the rewrite-engine to search for the next redex, or creates an
 ad-hoc theorem for rewriting, thus the programmer needs to adopt many
 technicalities of Isabelle, for instance, the \textit{Trueprop}
 constant.
 interpreter, where control is handed over to the user in interactive
 tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
 \medskip The above program also indicates the dominant role of interactive
 selection of knowledge in the three-dimensional universe of
-mathematics as depicted in Fig.\ref{fig:mathuni} on
+mathematics. The \texttt{SubProblem} in the above lines
-p.\pageref{fig:mathuni}, The \texttt{SubProblem} in the above lines
 {\rm 07..09} is more than a function call with the actual arguments
 \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
 three items:
 \begin{enumerate}

changeset 48766	7132779e2ff4
parent 42516	461f6d9d5390
child 48767	582caed78c5f