1.1 --- a/src/Tools/isac/Doc/ROOT Sat Dec 30 16:49:50 2023 +0100
1.2 +++ b/src/Tools/isac/Doc/ROOT Sat Dec 30 17:52:03 2023 +0100
1.3 @@ -22,6 +22,11 @@
1.4 theories
1.5 "Specify_Phase"
1.6 document_files
1.7 + "coil-kernel-uv.png"
1.8 + "Screenshot-problemdef-running-expl.png"
1.9 + "specification-complete.png"
1.10 + "specification-method.png"
1.11 + "specification-template.png"
1.12 "root.bib"
1.13 "root.tex"
1.14
2.1 --- a/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy Sat Dec 30 16:49:50 2023 +0100
2.2 +++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy Sat Dec 30 17:52:03 2023 +0100
2.3 @@ -7,10 +7,732 @@
2.4
2.5 text \<open>
2.6 \chapter{Interactive Specification in an \isac-Calculation}
2.7 +%#############################################################################
2.8 +This is a copy of the submission to the post-proceedings of ThEdu'23
2.9 +under the title \textit{``Interactive Formal Specification for Mathematical Problems of Engineers''} \footnote{
2.10 +\url{https://static.miraheze.org/isacwiki/a/a0/Wneuper-3-adopt-post.pdf)}}.
2.11 +Thus this chapter is preliminary, it will be supplemented and probably split
2.12 +up in the following.
2.13
2.14 -TODO
2.15 +\section{Introduction} \label{sect:introduction}
2.16 +%==============================================================================
2.17 +Since its beginnings more than two decades ago the \sisac{} project strives for
2.18 +a generally usable system for mathematics education, which might cover a major
2.19 +part of educational scenarios, posing and solving problems which can best be
2.20 +tackled by mathematical methods.
2.21 +%
2.22 +This paper presents the second part of a concise description of the prototype
2.23 +that has been developed in the course of the project, the description of the
2.24 +so-called specify-phase, while the first part describing the solve-phase is
2.25 +already published \cite{wn:lucin-thedu20}.
2.26 +
2.27 +\medskip
2.28 +The specify-phase first addresses the ``what to solve'', while the solve-phase
2.29 +addresses the ``how to solve'' later in the process of problem solving ---
2.30 +an important conceptual separation in
2.31 +the education of engineers. In terms of computer mathematics the fist
2.32 +phase concerns a transition from facts in the physical world (captured by
2.33 +text or figures) to abstract notions of mathematics (mainly captured by
2.34 +formulas). And in terms of educational science and psychology this first phase
2.35 +concerns a transition from intuitive and associative human thinking to
2.36 +handling of abstract formal entities according to formal logic.
2.37 +
2.38 +A successful transition results in a ``formal specification'' (to be exactly
2.39 +defined in \S\ref{ssec:urs-specify} Pt.\ref{UR:form-spec} on
2.40 +p.\pageref{UR:form-spec}), so the subsequent solve-phase resides
2.41 +exclusively in the abstract area of computater mathematics,
2.42 +where Lucas-Interpretation \cite{wn:lucin-thedu20} is
2.43 +able to automatically generate ``next step guidance'' \cite{gdaroczy-EP-13}
2.44 +and reliable checks of logical correctness --- this paper, however, addresses the
2.45 +preceding phase, more challenging in terms of computer mathematics and in terms
2.46 +of psychology.
2.47 +
2.48 +The latter point will be touched on in this paper only by relating it here to
2.49 +recent advances in Artifical Intelligence, where ChatCPT for instance,
2.50 +achieved great public attention, even among computer mathematicians
2.51 +\cite{bb-ChatCPT-2023}. A software, which given a textual description
2.52 +of mathematical problems is able to convincingly reason about relevant facts,
2.53 +to react to supplementary remarks and even come up with a solution for the problem
2.54 +\emph{and is able to justify the solution} --- doesn't it outperform software
2.55 +of formal mathematics, in particular, might it outperform the \sisac{} prototype?
2.56 +%
2.57 +In spite of this serious question, the present step of development in the \sisac{}
2.58 +project continues to build the prototype solely upon the proof assistant Isabelle
2.59 +\cite{LCF-to-Isabelle-HOL:2019}. Presently without systematic experiments and
2.60 +detailed examination, the
2.61 +\sisac{} project is aware, that integrations of AI technologies and formal
2.62 +mathematics are a vivid research topic (see, for instance,
2.63 +\cite{benzmuller-2021.7,jamnik-2023.2}). And the description of our
2.64 +conservative approach contains hints at a ``dialog guide'' and a ``user model'',
2.65 +which will be necessary to adapt the power of the \sisac{} protoype (and system,
2.66 +sooner or later) to the needs of the user, the student -- and in such future
2.67 +development the \sisac{} project will come back to AI.
2.68 +
2.69 +\medskip
2.70 +The present description, of how the \sisac{} prototype handles the specify-phase, is
2.71 +partly a position paper in that it omits the justification for user requirements
2.72 +(already published in \cite{imst-htl07,imst-htl06,imst-hpts08}) and not even
2.73 +evaluates them (which shall be more informative in a broader educational
2.74 +setting in the future). And partly the description reports technical details
2.75 +how design and implementation attempts to realise these requirements;
2.76 +a secondary objective of the description is to motivate the reuse of generic tools for
2.77 +language definition in proof assistants and their rich pool of software
2.78 +components for formal mathematics and also their front-ends ---
2.79 +and \emph{not} to re-invent the wheel again and again in educational math
2.80 +software development.
2.81 +
2.82 +The paper has another special feature, the lack of related work ---
2.83 +because there seems none to be to the best knowledge of the author. The ThEdu
2.84 +workshop series were
2.85 +founded to promote activities for the creation of software generally useful for
2.86 +mathematics education. There have been notable successes with geometry software
2.87 +and software to teach mechanical reasoning in academia, but software to support
2.88 +learning in the most general education settings, maths problem solving,
2.89 +still does not exist.
2.90 +
2.91 +\medskip
2.92 +There is an actual reason for writing this paper now: It became apparent
2.93 +that the Java-based front-end of the \sisac{} prototype cannot catch up with recent development
2.94 +of front-ends in mathematics software: proof assistants make semantic
2.95 +information transparent to the user, they make formulas a door
2.96 +open for a great portion of mathematics knowledge just by mouse-click.
2.97 +So this lead to the hard decision to drop the Java-based front-end,
2.98 +i.e. about thirty valuable student projects
2.99 +\footnote{\url{https://isac.miraheze.org/wiki/Credits}} and to start
2.100 +shifting \sisac's code in between Isabelle's proof machinery and Isabelle's
2.101 +upcoming new front-end Isabelle/VSCode.
2.102 +The first step in this shift is additionally motivated by a lucky technical
2.103 +coincidence: Isabelle's formulas (terms, in respective diction) are \emph{linear}
2.104 +sequences of (very specific) characters -- and so are formulas on the Braille
2.105 +display\footnote{\url{https://en.wikipedia.org/wiki/Refreshable_braille_display}}.
2.106 +Thus \sisac{} engages in the ``A-I-MAWEN'' project aiming at an
2.107 +\textbf{A}ccessible \footnote{\url{https://en.wikipedia.org/wiki/Accessibility}}
2.108 +and \textbf{I}nclusive\footnote{\url{https://en.wikipedia.org/wiki/Inclusion_(education)}}
2.109 +\textbf{Ma}thematics \textbf{W}orking \textbf{En}vironment
2.110 +taking advantage from VSCode's accessibility features; and Isabelle enjoys
2.111 +collaboration on its upcoming new new front-end \cite{mawen-23,IsaWS-22}.
2.112 +
2.113 +\paragraph{The paper is organised as follows.}
2.114 +After the introduction first come user requirements, as clarified in the
2.115 +\sisac{} project. The requirements are partitioned in general ones in
2.116 +\S\ref{ssec:urs-gerneral} and ones addressing the specify-phase in
2.117 +\S\ref{ssec:urs-specify}.
2.118 +
2.119 +After a definition of ``formal specification'' the design of interaction
2.120 +in the specify-phase
2.121 +is described by use of a running example given in \S\ref{ssec:running-expl}.
2.122 +\S\ref{ssec:formalise} describes the transition from text and
2.123 +figures into formal mathematics, \S\ref{ssec:variants} turns to the most
2.124 +essential features, freedom in input and freedom to pursuevariants in
2.125 +problem solving. \S\ref{ssec:interactivity} shows, what kinds of feedback can
2.126 +be given in the specify-phase. And \S\ref{ssec:auto-spec} addresses problem-refinement,
2.127 +a particularly sketchy part in the \sisac{} prototype. The final section
2.128 +\S\ref{ssec:solve-phase} concerns the transition from the specify-phase to the
2.129 +solve-phase.
2.130 +
2.131 +\medskip
2.132 +Since the paper also wants to advertise the generic tools of proof assistants
2.133 +for defining new input languages, in particular the tools of Isabelle, the
2.134 +section on implementation is detailed as follows.
2.135 +\S\ref{ssec:outer-syntax} shows how elegantly \sisac's input language for
2.136 +the specify-phase can be
2.137 +implemented in Isabelle/Isar, \S\ref{ssec:interaction} goes into detail with
2.138 +handling semantics of the input. Analogously to the solve-phase also the
2.139 +specify-phase is organised in steps introduced in \S\ref{ssec:stepwise}.
2.140 +A specific detail is refinement of equations discussed in \S\ref{ssec:refine}.
2.141 +\S\ref{ssec:efficiency} addresses efficiency considerations and finally
2.142 +in \S\ref{ssec:preconds} preconditions are described, which require evaluation
2.143 +by rewriting.
2.144 +\S\ref{sect:conclusion} gives a brief summary and concludes the paper.
2.145 +
2.146 +
2.147 +
2.148 +\section{User Requirements} \label{sect:user-requirements}
2.149 +%==============================================================================
2.150 +\sisac{} aims at an educational software and so design and development started
2.151 +with analysing the requirements, which a student places on the system when
2.152 +using it according to the introduction.
2.153 +The requirements capture and requirements analysis in the \sisac{} project
2.154 +\footnote{\url{https://isac.miraheze.org/wiki/History}}
2.155 +are already published in \cite{imst-htl07,imst-htl06,imst-hpts08}.
2.156 +Here the requirements
2.157 +\footnote{This list will go into the \sisac{} documentation and
2.158 +supersedes the old documentation \cite{isac:all}}.
2.159 +are kept as short as possible, are restricted to the specify-phase
2.160 +and serve to introduce the system features from the users point of view;
2.161 +the descriptions of respective implementation details
2.162 +in \S\ref{sect:design} justify the requirements more or less explicitly by
2.163 +backward references. However, first come some general considerations.
2.164 +
2.165 +\subsection{Foundational axioms about User Requirements}\label{ssec:urs-gerneral}
2.166 +%------------------------------------------------------------------------------
2.167 +\sisac's decision to build software on top of reasoning technology -- for maths
2.168 +education at high school and academic engineering courses, this decision is
2.169 +novel and opens up novel educational settings.
2.170 +The efficiency of these setting shall be researched thoroughly. As soon as
2.171 +tracing data\footnote{There
2.172 +are good experiences with logging user-interaction in \sisac{} \cite{fkober-bakk}}
2.173 +from the interaction with such tools become available, interesting
2.174 +discussions in educational research of mathematics education can be expected.
2.175 +
2.176 +
2.177 +Until then the following requirements are considered as abstract and so far from
2.178 +concrete usability testing that these requirements are stated as axioms,
2.179 +axioms advocating software models to learn by interaction, \emph{not} to
2.180 +learn by a teachers explanation primarily:
2.181 +
2.182 +\begin{itemize}
2.183 +\item\textbf{A complete model of mathematics} shall comprise all software tools
2.184 +required to solve a problem at hand, such that a student need not switch
2.185 +between different software applications: the problem statement, the textbook with
2.186 +background theory and explanation, the formulary, probably another textbook
2.187 +with a boilerplate for solving the problem at hand, and last not least an electronic
2.188 +notebook for interactive construction of a solution for the problem.
2.189 +
2.190 +\item\textbf{A transparent model of mathematics} shall be open for all kinds of
2.191 +inquiry of the underlying maths knowledge: What data is required to probably
2.192 +describe a given problem? What is required as input, what is expected as output?
2.193 +What are the types of the respective data types? What are the constraints
2.194 +(preconditions) on the input? What pattern does the problem at hand match,
2.195 +what are similar problems? And at the transition to the solve-phase there
2.196 +are further questions to be answered by the system: Which methods could be
2.197 +appropriate for finding a solution? Etc.
2.198 +
2.199 +\item\label{axiom:stepwise-inter}\textbf{An interactive model of mathematics}
2.200 +shall support step-wise construction of a solution to a given problem.
2.201 +Each step is checked for correctness and justified according to the above
2.202 +axiom of ``transparency''.
2.203 +So interaction follows the principle of ``correct by construction''.
2.204 +\end{itemize}
2.205 +
2.206 +\noindent
2.207 +\sisac's basic design is not embossed to mimic a human lecturer or teacher,
2.208 +rather the student shall learn independently from a software model, which
2.209 +clearly represents an essence of mathematics.
2.210 +In fact, if mathematics is the ``science to mechanise thinking'' (Bruno Buchberger
2.211 +\footnote{\url{https://en.wikipedia.org/wiki/Bruno_Buchberger}}), then this
2.212 +science is most appropriate one to be modelled on computers, essentials can
2.213 +be best studied there and prover technologies provide the most
2.214 +powerful tools \cite{EPTCS290.6} for developing tools, which give justifications
2.215 +and explanations.
2.216 +
2.217 +Experiences with \sisac{} indicate that the hint of ``mechanises thinking''
2.218 +is helpful for students at any age, helpful to chase the omnipresent suspicion that
2.219 +mathematics is magic. Just watch a power user of a proof assistant, how she or
2.220 +he plays around with text snippets in order to find solutions (after a coarse
2.221 +idea of a subject matter or a proof has become clear).
2.222 +
2.223 +\subsection{User Requirements focusing Specify-Phase} \label{ssec:urs-specify}
2.224 +%------------------------------------------------------------------------------
2.225 +Now, what follows are the requirements which serve to pass the specify-phase
2.226 +successfully, to come from human imagination of a problem (triggered by an
2.227 +informal text or a figure or whatever) to a formal representation, appropriate
2.228 +to be tackled within software.
2.229 +
2.230 +\begin{enumerate}
2.231 +\item As an educational software \sisac{} must be \textbf{intuitive} such that a
2.232 +newbie can easily learn to use the system by interacting with trial and error.
2.233 +
2.234 +\item\label{UR:form-spec} The system ensures ``correctness by construction''
2.235 +when given a \textbf{formal specification} (definition):
2.236 +%\begin{definition}
2.237 +Two lists of terms are given, input $\it{in}$ and output $\it{out}$.
2.238 +And given are two predicates: The precondition $\it{Pre}\;(\it{in})$ constrains
2.239 +the elements of the input to reasonable values. The postcondition
2.240 +$\it{Post}\;(\it{in},\,\it{out})$ relates input and output
2.241 +(and thus characterises the kind of problem).
2.242 +%\end{definition}
2.243 +
2.244 +\medskip
2.245 +This definition is according to \cite{gries} and restricts the kind of problems
2.246 +accepted by the system.
2.247 +
2.248 +\item\label{UR:next-step}If a student gets stuck, the system can
2.249 +\textbf{propose a next step}, i.e. a single element of the specification,
2.250 +which is still missing (equivalent to Lucas-Interpretation \cite{wn:lucin-thedu20}).
2.251 +
2.252 +\item\label{UR:types} \sisac{} tries to raise students awareness of different
2.253 +operational power in different number ranges (e.g. in the complex numbers
2.254 +each polynomial has roots, in the real numbers it may have none).
2.255 +Thus it \textbf{restricts Isabelle's contexts to
2.256 +particular theories}, for instance to \texttt{Int.thy}, to \texttt{Real.thy} or
2.257 +to \texttt{Complex.thy}.
2.258 +
2.259 +\item\label{UR:model} \textbf{No need for formal logic}:
2.260 +The formal specification of a problem must be
2.261 +comprehensible for students in an academic course in engineering disciplines
2.262 +(and also at high school) without any instruction in formal logic. So a
2.263 +\emph{Specification} is given by \emph{Given} (the input according to
2.264 +Pt.\ref{UR:form-spec}),
2.265 +\emph{Where} (the precondition) and \emph{Find} (the output, i.e. the solution
2.266 +of the problem) and \emph{Relate} (to be described in the next point).
2.267 +
2.268 +\item\label{UR:relate}\textbf{\emph{Relate}} captures essential parts of the postcondition
2.269 +such that the description avoids logical operators (like $\exists$,
2.270 +$\forall$, $\land$, $\lor$ etc) according to requirement \UR\ref{UR:model}.
2.271 +This is a crucial design decision of \sisac{} which will be illustrated
2.272 +by the running example.
2.273 +
2.274 +\item\label{UR:variants}In general, mathematical problems can be solved in many
2.275 +ways. Thus a \emph{Specification} must be \textbf{open for variants} which are
2.276 +handled within one and the same process of solving the problem. The running
2.277 +example (\S\ref{ssec:variants} below) illustrates three variants.
2.278 +
2.279 +\item\label{UR:template} The transition from an informal problem description,
2.280 +given by text and by figures, to the formal specification must not be
2.281 +overstrained by \textbf{issues of formal notation}. The problem is well-known from
2.282 +educational use of algebra systems \cite{fuchs:algebra-sys}. Thus \sisac{} will
2.283 +give the following templates for the respective types (examples are given in
2.284 +Fig.\ref{fig:specification-template} below):
2.285 +\begin{itemize}
2.286 +\item $[$\_\_=\_\_, \_\_=\_\_$]$ for lists of equalities,
2.287 + for example ${\it Constants }\,[a=1, b=2]$
2.288 +\item $[$\_\_, \_\_$]$ for lists of elements without $=$,
2.289 + for example ${\it AdditionalValues }\,[a, b, c]$
2.290 +\item "\_\_" for theories (as strings),
2.291 + for example ${\it Theory\_Ref}\;{\it"Diff\_App"}$
2.292 +\item "\_\_/\_\_" for string lists,
2.293 + for example ${\it Problem\_Ref}\;{\it"univariate\_calculus/optimisation"}$
2.294 +\item \_\_ for arbitrary input (not involving the above cases),
2.295 + for example ${\it Maximum\;A}$.
2.296 +\end{itemize}
2.297 +
2.298 +\item\label{UR:toggle-problem-method} Within the \emph{Specification} the
2.299 +\textbf{\emph{Model} serves two purposes}: for the \emph{Problem\_Ref} it shows
2.300 +the fields from \emph{Given} to \emph{Relate} according to Pt.\ref{UR:model}
2.301 +and for \emph{Method\_Ref} it shows the guard of the program guiding
2.302 +the \emph{Solution}; for details see \cite{wn:lucin-thedu20}. A
2.303 +toggle switches between the two purposes (in the examples below indicated by
2.304 +$\otimes$ and $\odot$, the former for activation and the latter for idle).
2.305 +
2.306 +\item\label{UR:toggle}The \textbf{specify-phase can be skipped} on predefined
2.307 +settings. This requirement is more important than it seems: \sisac{} may be
2.308 +not only be used for solving new problems, but also for exercising \emph{known}
2.309 +problems, for instance differentiation. In that case \emph{Specification}
2.310 +will be folded in such that the solve-phase will be started immediately
2.311 +by \emph{Solution}.
2.312 +
2.313 +\item\label{UR:complete}A \emph{Specification} \textbf{can be completed} automatically
2.314 +(by pushing a button or the like), in case a student wants to enter the solve-phase
2.315 +right now (and in case the course designer allows to do so by the predefined
2.316 +settings).
2.317 +
2.318 +\item\label{UR:refine}In equation solving the system can \textbf{assist in finding an
2.319 +appropriate type of equation}. That means, in this special case the system
2.320 +is capable of problem refinement (which is under ongoing research on more
2.321 +general problem types). The user requests this assistance by easy-going means
2.322 +(by pushing a button or the like).
2.323 +
2.324 +\item\label{UR:feedback}There is the following \textbf{feedback on a
2.325 +specification's elements}, indicated at the appropriate location of the
2.326 +respective element on screen:
2.327 + \begin{itemize}
2.328 + \item \textbf{Correct}: There is probably no specific indication.
2.329 + \item \textbf{Syntax}: This feedback can be necessary, if the user
2.330 + switches the \emph{Model} suddenly from \emph{Problem\_Ref} to
2.331 + \emph{Method\_Ref} or vice versa, see \UR\ref{UR:toggle-problem-method}
2.332 + \item \textbf{Incomplete}: Input is incomplete, in particular elements
2.333 + of type list.
2.334 + \item \textbf{Superfluous}: An input can be syntactically correct, but have no
2.335 + evident relation to the problem at hand.
2.336 + \end{itemize}
2.337 +
2.338 +%\item TODO
2.339 +%\item TODO
2.340 +\end{enumerate}
2.341 +
2.342 +\noindent
2.343 +These user requirements evolved alongside two decades of development in the
2.344 +\sisac{} project, which was close to educational practice all the time due to
2.345 +%ref.2: confusing ^v^v^
2.346 +the involved persons; and the requirements have been checked in several field
2.347 +tests \cite{imst-htl07,imst-htl06,imst-hpts08}.
2.348 +
2.349 +The requirements raise a lot of questions with respect to detailed
2.350 +software design. Some of the questions will be clarified alongside presenting
2.351 +the running example in \S\ref{sect:design} below.
2.352 +
2.353 +
2.354 +\section{Design of the Specify-Phase} \label{sect:design}
2.355 +%==============================================================================
2.356 +In the specify-phase a student interactively constructs a formal specification
2.357 +(definition
2.358 +in \S\ref{ssec:urs-specify} Pt.\ref{UR:form-spec} on p.\pageref{UR:form-spec}),
2.359 +which then enables Lucas-Interpretation \cite{wn:lucin-thedu20} to
2.360 +automatically generate user guidance.
2.361 +The concept of formal specification involves logic, which is not taught at
2.362 +many engineering faculties (and not at all at high school), however.
2.363 +Thus, according to \S\ref{ssec:urs-specify} requirement no.\ref{UR:form-spec}
2.364 +on p.\pageref{UR:form-spec}, respective logic is hidden from the user;
2.365 +for explaining that approach we use a running example.
2.366 +
2.367 +\subsection{A Running Example} \label{ssec:running-expl}
2.368 +%------------------------------------------------------------------------------
2.369 +The running example is re-used from \cite{mawen-23}: There it was used to
2.370 +illustrate what has been achieved in the old prototype and what is
2.371 +\emph{planned} for developing a ``mathematical working environment'', whereas in
2.372 +this paper the example is used to explain the design and implementation
2.373 +of the part of the prototype supporting the specify-phase.\\
2.374 +
2.375 +\begin{minipage}[c]{0.55\textwidth}
2.376 +% first column
2.377 +\textit{
2.378 +The efficiency of an electrical coil depends on the mass of the kernel.
2.379 +Given is a kernel with cross-sectional area, determined by two rectangles of
2.380 +the same shape as shown in the figure.\\
2.381 +Given a radius $r=7$, determine the length~$u$ and width~$v$ of the rectangles
2.382 +such that the cross-sectional area~$A$ (and thus the mass of the kernel) is a
2.383 +maximum.}\\
2.384 +\end{minipage}
2.385 +\hfill
2.386 +%second column
2.387 +\begin{minipage}{0.45\textwidth}
2.388 + \includegraphics[width=0.55\textwidth]{coil-kernel-uv.png}\\
2.389 +\end{minipage}
2.390 +In ancient times this kind of example belonged to a well-established class of
2.391 +examples at the end of the mathematics curriculum at German speaking Gymnasiums,
2.392 +``Extremwertaufgaben''. Nowadays it can be found in text books for electrical
2.393 +engineering.
2.394 +
2.395 +\subsection{Formalisation of Problems and Authoring} \label{ssec:formalise}
2.396 +%------------------------------------------------------------------------------
2.397 +In order to meet \UR\ref{UR:next-step} it is necessary to prepare data for
2.398 +each example, where automated generation of user guidance is desired
2.399 +\cite{wn:lucas-interp-12}. Classes of examples are collected to \textit{Problem}s;
2.400 +this conforms with teaching experience:
2.401 +certain classes focus on certain problem patterns, which are
2.402 +explained and exercised by more or less different examples.
2.403 +%ref.2: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ confusing
2.404 +
2.405 +Most of the lecturers and teachers want to expose their \emph{personal} collection of
2.406 +exercises to their students; so lecturers should be enabled to implement these
2.407 +independently in the system, without further expertise -- so \emph{authoring for
2.408 +lecturers} needs to be supported eventually for type \texttt{Formalise.T}
2.409 +below. However, the implementation of problem patterns \texttt{Model\_Pattern.T}
2.410 +involves specific knowledge in computer mathematics --
2.411 +so \emph{maths authoring} needs to be supported in addition, eventually.
2.412 +%ref.2: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ repetitive/ confusing
2.413 +``Maths authors'' might be lecturers of specific academic courses,
2.414 +book authors and others.
2.415 +
2.416 +%ref.2:-----------vvvvvvvvvv what distinction?
2.417 +According to this distinction there are the following two data-types
2.418 +\footnote{We adapt ML \cite{pl:milner97} syntax for readability purposes:
2.419 +instead of "type T in structure Formalise" we write "Formalise.T". "(*" and "*)"
2.420 +enclose comments, which are outside ML syntax. The numbers on the left margin
2.421 +serve referencing and do not belong to the ML code.}:
2.422 +
2.423 +\begin{small}
2.424 +\begin{verbatim}
2.425 + 01 type Formalise.T = model * refs;
2.426 +\end{verbatim}
2.427 +\end{small}
2.428 +\label{src:model-pattern}
2.429 +\begin{small}
2.430 +\begin{verbatim}
2.431 + 01 type Model_Pattern.T =
2.432 + 02 (m_field * (* field "Given", "Find", "Relate" *)
2.433 + 03 (descriptor * (* for term *)
2.434 + 04 term)) (* identifier for instantiating term *)
2.435 + 05 list;
2.436 + 06 (*does NOT contain preconditions "Where"; these have no descriptor*)
2.437 +\end{verbatim}
2.438 +\end{small}
2.439 +
2.440 +The \texttt{type Formalise.T} consists of a (preparatory form of) model and
2.441 +\texttt{refs}; the latter are explained below in \S\ref{ssec:solve-phase}.
2.442 +\texttt{Model\_Pattern.T} is designed according to \UR\ref{UR:model}.
2.443 +Each \texttt{term}
2.444 +is accompanied by a \texttt{descriptor}, which informs the user about what
2.445 +is requested from him to input. Pairs of \texttt{(descriptor * term)} are
2.446 +assigned to \texttt{m\_field}s according to \UR\ref{UR:model}.
2.447 +The special values for the running example
2.448 +are as follows, where the \texttt{descriptor}s are \texttt{Constants},
2.449 +\texttt{Maximum}, \texttt{AdditionalValues}, \texttt{Extremum},
2.450 +\texttt{SideConditions}, \texttt{FunctionVariable}, \texttt{Domain}
2.451 +and \texttt{ErrorBound}:
2.452 +
2.453 +\begin{small}
2.454 +\begin{verbatim}
2.455 + 01 val demo_example = ("The efficiency of an electrical coil depends on the mass of the kernel. Given is a kernel with cross-sectional area determined by two rectangles of same shape as shown in the figure. Given a radius r = 7, determine the length u and width v of the rectangles such that the cross-sectional area A (and thus the mass of the kernel) is a maximum. + Figure",
2.456 + 02 ([
2.457 + 03 (*Problem model:*)
2.458 + 04 "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
2.459 + 05 "Extremum (A = 2 * u * v - u \<up> 2)",
2.460 + 06 "SideConditions [((u::real) / 2) \<up> 2 + (v / 2) \<up> 2 = r \<up> 2]",
2.461 + 07 "SideConditions [(u::real) / 2 = r * sin \<alpha>, v / 2 = r * cos \<alpha>]",
2.462 + 08 (*MethodC model:*)
2.463 + 09 "FunctionVariable u", "FunctionVariable v",
2.464 + 10 "FunctionVariable \<alpha>",
2.465 + 11 "Domain {0 <..< r}",
2.466 + 12 "Domain {0 <..< \<pi> / 2}",
2.467 + 13 "ErrorBound (\<epsilon> = (0::real))"]: TermC.as_string list,
2.468 + 14 ("Diff_App", ["univariate_calculus", "Optimisation"],
2.469 + 15 ["Optimisation", "by_univariate_calculus"]): References.T)): Formalise.T
2.470 +\end{verbatim}\label{src:demo-expl}
2.471 +\end{small}
2.472 +The text in line \texttt{01} exceeds the line limit, it has already been
2.473 +shown with the problem statement of the running example in \S\ref{ssec:running-expl}.
2.474 +The reader may be surprised by the multiple entries for the descriptors
2.475 +\texttt{SideConditions}, \texttt{FunctionVariable} and \texttt{Domain};
2.476 +this is due to \emph{variants} introduced in \S\ref{ssec:variants} below ---
2.477 +this representation of variants is considered intermediate, it was easy
2.478 +to implement and will be up to further refinement. The lines \texttt{14} and
2.479 +\texttt{15} represent the \texttt{refs} introduced above in \texttt{Formalise.T}
2.480 +and explained in \S\ref{ssec:solve-phase} below.
2.481 +The attentive reader will also notice that the items of the example's \texttt{model}
2.482 +are not assigned to an \texttt{m\_field}
2.483 +(line \texttt{02} on p.\pageref{src:model-pattern}), rather the
2.484 +\texttt{descriptor} is the means to relate items between different data
2.485 +structures, in this case between \texttt{Formalise.model} and the
2.486 +\texttt{problem} below defining the running example:
2.487 +\begin{small}
2.488 +\begin{verbatim}
2.489 + 01 problem pbl_opti_univ : "univariate_calculus/Optimisation" =
2.490 + 02 \<open>eval_rls\<close> (*for evaluation of 0 < r*)
2.491 + 03 Method_Ref: "Optimisation/by_univariate_calculus"
2.492 + 04 Given: "Constants fixes"
2.493 + 05 Where: "0 < fixes"
2.494 + 06 Find: "Maximum maxx" "AdditionalValues vals"
2.495 + 07 Relate: "Extremum extr" "SideConditions sideconds"
2.496 +\end{verbatim}\label{problem}
2.497 +\end{small}
2.498 +The above \texttt{problem} assigns the elements of the model (in \sisac{} we
2.499 +call an element of a model an \emph{item} in order not to confuse with
2.500 +\emph{elements} of lists or sets) to a respective \texttt{m\_field}.
2.501 +As already mentioned, the assignment is done via \texttt{descriptor}s accompanied with
2.502 +place-holders (\texttt{fixes}, \texttt{maxx}, etc; see line \texttt{03}
2.503 +in \texttt{type Model\_Pattern.T} on p.\pageref{src:model-pattern}) -- these are instantiated
2.504 +on the fly with values of the concrete example selected by the user.
2.505 +
2.506 +It is the task of a mathematics author to decide the structure
2.507 +of the model such that it covers an appropriate collection of examples,
2.508 +where a respective \texttt{Model\_Pattern.T} of a \texttt{problem} is
2.509 +instantiated for several examples by values of a \texttt{Formalise.T}.
2.510 +For instantiation of the model for a \texttt{problem} an environment is
2.511 +required, for instance for the \texttt{demo\_example} the environment
2.512 +\label{env-subst}
2.513 +\begin{small}
2.514 +\begin{tabbing}
2.515 +12345\=$[$x\=$($\kill
2.516 +\>[\>$("fixes", \;[r = 7]), \;\;("maxx", \;A), \;\;("vals", \;[u, v]),$\\
2.517 +\> \>$("extr", \;(A = 2 * u * v - u \uparrow 2)), \;\;
2.518 + ("sideconds", \;[(u / 2) \uparrow 2 + (v / 2) \uparrow 2 = r \uparrow 2])$\\
2.519 +\>]
2.520 +\end{tabbing}
2.521 +\end{small}
2.522 +is required.
2.523 +
2.524 +Another reason for this late assignment is that one and the same item may
2.525 +belong to \texttt{m\_field} \texttt{Relate} for a problem but to \texttt{Given}
2.526 +for a \texttt{method}, see \S\ref{ssec:solve-phase}.
2.527 +Finally it may be remarked that the identifier
2.528 +\texttt{"univariate\_calculus/Optimisation"} can be found in a more
2.529 +convenient format already on p.\pageref{src:demo-expl} on line \texttt{14}).
2.530 +
2.531 +
2.532 +\subsection{Freedom of Input and Variants in Problem Solving} \label{ssec:variants}
2.533 +%------------------------------------------------------------------------------
2.534 +The model described above is presented
2.535 +\footnote{\S\ref{ssec:outer-syntax} will show how easily the format presented
2.536 +in the screen-shot can be defined in Isabelle/Isar.}
2.537 +to students as shown in the screen-shot
2.538 +% on p.\pageref{fig:specification-template}.
2.539 +below.
2.540 +\begin{figure} [htb]
2.541 + \centering
2.542 + \includegraphics[width=0.6\textwidth]{specification-template.png}
2.543 + \caption{The template for starting a \emph{Specification}.}
2.544 + \label{fig:specification-template}
2.545 +\end{figure}
2.546 +There the \texttt{descriptor}s (\texttt{Constants}, etc) are followed by
2.547 +templates giving hints on the input format according to
2.548 +\UR\ref{UR:template} in order to help students to cope with the troublesome
2.549 +transition to exact formal representation. The \texttt{Model} is embedded
2.550 +into the \texttt{Specification} which also contains \texttt{References}
2.551 +explained in \S\ref{ssec:solve-phase} below. The above template is completed
2.552 +in Fig.\ref{fig:specification-complete} on p.\pageref{fig:specification-complete}
2.553 +and the reader may refer to the \texttt{Relate} in the \texttt{Model} when
2.554 +reading the next paragraph.
2.555 +
2.556 +\subparagraph{Representation in field \texttt{Relate} is simplified}\label{post-cond}
2.557 +such that a student needs not encounter formal logic according to \UR\ref{UR:relate}.
2.558 +Fig.\ref{fig:specification-complete} %on p.\pageref{fig:specification-complete}
2.559 +shows that for the \texttt{demo\_example}
2.560 +\texttt{Extremum} and \texttt{SideConditions} actually are the
2.561 +essential parts of the postcondition, which characterises a \texttt{problem}
2.562 +by relating \texttt{Given} and \texttt{Find}:
2.563 +\begin{eqnarray*}
2.564 + &\;& (A = 2 * u * v - u \uparrow 2)\;\;\land\;\;
2.565 + ((u / 2) \uparrow 2 + (v / 2) \uparrow 2 = r \uparrow 2)\;\;\land\\
2.566 +\forall A' u' v'
2.567 + &.&
2.568 + (A' = 2 * u' * v' - u' \uparrow 2)\;\land\;
2.569 + ((u' / 2) \uparrow 2 + (v' / 2) \uparrow 2 = r \uparrow 2)\;\;
2.570 + \Rightarrow A' < A
2.571 +\end{eqnarray*}\label{postcondition}
2.572 +Students at engineering faculties usually are not educated in formal logic
2.573 +(computer science is an exception). A formula containing $\land$ or $\Rightarrow$ would distract
2.574 +them from actual problem solving. Thus \sisac{} decided to extract the essential
2.575 +parts of the postcondition:
2.576 +\begin{tabbing}
2.577 +12345\=\kill
2.578 +\> \texttt{Extremum} $(A = 2 * u * v - u \uparrow 2)$,
2.579 + \texttt{SideConditions} $(u / 2) \uparrow 2 + (v / 2) \uparrow 2 = r \uparrow 2$
2.580 +\end{tabbing}
2.581 +These parts also are sufficient to automatically generate user-guidance
2.582 +according to \UR\ref{UR:next-step} (by enabling Lucas-Interpretation
2.583 +\cite{wn:lucas-interp-12} to find a next step).
2.584 +
2.585 +\bigskip
2.586 +Input should not only be easygoing with respect to format and with bypassing formal
2.587 +logic. According to \UR\ref{UR:variants} the system should cope flexibly with
2.588 +semantics, it should also adapt to fresh ideas of a student and support various
2.589 +variants in solving a particular problem.
2.590 +Let us look at Fig.\ref{fig:specification-complete} with the completed
2.591 +\texttt{Specification} and ask an important question:
2.592 +\begin{figure} [htb]
2.593 + \centering
2.594 + \includegraphics[width=0.65\textwidth]{specification-complete.png}
2.595 + \caption{The complete \emph{Specification}.}
2.596 + \label{fig:specification-complete}
2.597 +\end{figure}
2.598 +What could a student have in mind when encountering the problem
2.599 +statement on p.\pageref{ssec:running-expl}? Looking at the figure
2.600 +on p.\pageref{ssec:running-expl}, he or she
2.601 +might focus on the width $u$ and the length $v$, and apply Pythagoras theorem
2.602 +$(u / 2) \uparrow 2 + (v / 2) \uparrow 2 = r \uparrow 2$.
2.603 +But students might focus as well on the angle $\alpha$ and formalise
2.604 +the \texttt{SideConditions} as $u / 2 = r * \sin \alpha,\;v / 2 = r * \cos \alpha$.
2.605 +
2.606 +\medskip
2.607 +And what if a student has an eye for simple solutions and takes as
2.608 +\texttt{SideConditions} either $u = \cos\alpha, v = \sin\alpha$ or
2.609 +$u \uparrow 2 + v \uparrow 2 = 4 * r \uparrow 2$ ? The latter is semantically
2.610 +equivalent (equivalent in this specific example) to the variant shown in
2.611 +Fig.\ref{fig:specification-complete}. So, during the whole specify-phase,
2.612 +each formula input by a student must be checked for equivalence with the
2.613 +formulas prepared in the \texttt{Formalise.T}. Such checking is done via
2.614 +rewriting to a normal form. This might be quite tedious, for instance with
2.615 +equations involving fractions like in showing equivalence of the equations
2.616 +$u \uparrow 2 + v \uparrow 2 = 4 * r \uparrow 2
2.617 +\;\equiv\;
2.618 +(\frac{u}{2}) \uparrow 2 + (\frac{v}{2}) \uparrow 2 = r \uparrow 2$)
2.619 +
2.620 +\paragraph{An open design question, a ``pattern-matching-language'' ?}
2.621 +Now we are ready to address the design decision related to the format given
2.622 +on p.\pageref{src:demo-expl}, which has been identified as preliminary
2.623 +and simplistic for the purpose of simple implementation.
2.624 +Much information is redundant there, apparently, and on the other hand interesting
2.625 +structural properties are hardly visible. For instance, the student's decision
2.626 +whether to take the \texttt{FunctionVariable u} or the
2.627 +\texttt{FunctionVariable v} for differentiation (see \S\ref{ssec:solve-phase}),
2.628 +this decision is fairly independent from the \texttt{problem}'s model --
2.629 +the \texttt{Model} just must no refer to $\alpha$.
2.630 +
2.631 +The need for a separated language for \texttt{Specification} becomes definitely
2.632 +clear when considering the precondition and the postcondition (the latter
2.633 +introduced above on p.\pageref{postcondition}). The precondition must evaluate
2.634 +to true for a \texttt{Specification} to be valid, and the postcondition must be
2.635 +true for a \texttt{Solution} to be accepted by the system.
2.636 +
2.637 +In order to evaluate precondition \texttt{Where} $0 < r$ to true, we need to
2.638 +create the environment $[(r, 7)]$ from \texttt{Constants}. With the
2.639 +\texttt{demo\_example} this is straight forward, but if we had
2.640 +\texttt{Constants [s = 1, t = 2]} we already need to employ some trickery with
2.641 +indexing. And what about the postcondition?
2.642 +\begin{tabbing}
2.643 +123 \= $\forall \;\; {\it maxx}' \;\; {\it funvar}'\;\; . \;\;$ \=\kill
2.644 +\> \> ${\it extr} \;\;\land\;\; {\it sideconds}\;\;\land$ \\
2.645 +\> $\forall \;\; {\it maxx}' \;\; funvar'. \;\;$
2.646 + \> ${\it extr}' \;\land\; {\it sideconds}' \;\;
2.647 + \Rightarrow {\it maxx}' < {\it maxx}$
2.648 +\end{tabbing}
2.649 +How could such a ``pattern-matching'' description be instantiated to the
2.650 +postcondition on p.\pageref{postcondition}? Instantiated reliably, such that Isabelle could
2.651 +evaluate it to true with the values found by \texttt{Solution}? How would the
2.652 +variant with the $\alpha$ work out, which has two \texttt{SideConditions}?
2.653 +
2.654 +\medskip
2.655 +Answering the open question above may go in parallel to implementation of a larger
2.656 +body of examples and respective \texttt{problem}s.
2.657 +Field tests \cite{imst-htl06,imst-htl07,imst-hpts08} in the \sisac{} project
2.658 +were based on limited content and thus did not gain much experience with a
2.659 +variety of problems with variants and respective flexibility of the system;
2.660 +one has to wait for implementation of more various examples and problems.
2.661 +
2.662 +\subsection{Interactivity and Feedback} \label{ssec:interactivity}
2.663 +%------------------------------------------------------------------------------
2.664 +The previous section describes how \sisac{} makes a \texttt{Specification}
2.665 +flexible and open for various variants in solving a particular problem.
2.666 +Flexibility in problem solving must be accompanied by flexible interactivity
2.667 +and appropriate feedback. Feedback for input to a \texttt{Model} is
2.668 +predefined by \UR\ref{UR:feedback} and modelled by a respective datatype as
2.669 +follows (\texttt{values} are of type \texttt{term list})
2.670 +\begin{small}
2.671 +\begin{verbatim}
2.672 + 01 datatype I_Model.feedback =
2.673 + 02 Correct of (descriptor * values) (* wrt. syntax and semantics *)
2.674 + 03 | Incomplete of (descriptor * values) (* for list types *)
2.675 + 04 | Superfluous of (descriptor * values) (* not found in Formalise.model *)
2.676 + 05 | Syntax of TermC.as_string (* in case of switching model *)
2.677 +\end{verbatim}\label{src:feedback}
2.678 +\end{small}
2.679 +The above code plus comments appear fairly self-explaining. \texttt{descriptor}
2.680 +has been introduced already. In case of empty input, we shall have
2.681 +\texttt{Incomplete (\_, [])} and display templates for input-format
2.682 +according to \UR\ref{UR:template}. Syntax errors are handled very elegantly in
2.683 +Isabelle/PIDE (see \S\ref{ssec:outer-syntax}); in case of switching from the
2.684 +\texttt{Model} of the \texttt{Problem\_Ref} to the \texttt{Model} of the
2.685 +\texttt{Method\_Ref} (see \S\ref{ssec:solve-phase} below) it might be useful
2.686 +to keep a copy of an input with syntax errors. Items can be \texttt{Superfluous}
2.687 +either because they are syntactically correct but not related the \texttt{Model}
2.688 +under construction, or they belong to a \texttt{variant}, which has not yet been
2.689 +decided for. For instance, if the \texttt{Model} is as in
2.690 +Fig.\ref{fig:specification-complete} on p.\pageref{fig:specification-complete}
2.691 +and the student adds \texttt{SideConditions} $[v = \sin\alpha]$, this item
2.692 +will be marked as \texttt{Superfluous} unless interactive
2.693 +completion to \texttt{SideConditions} $[v = \sin\alpha, v = \cos\alpha]$
2.694 +and deletion of a competing item like \texttt{SideConditions}
2.695 +$[u \uparrow 2 + v \uparrow 2 = 4 * r \uparrow 2]$.
2.696 +
2.697 +\bigskip
2.698 +If a student gets stuck during input to a \texttt{Model}, then \UR\ref{UR:next-step}
2.699 +allows him or her to request help. In the specify-phase such help is given
2.700 +best by presenting a (partial -- predefined setting!) missing item.
2.701 +\emph{But output of a \texttt{Model} with item does not conform to Isabelle's
2.702 +document model}: The content of an Isabelle theory is considered a document
2.703 +which has to be checked by the system --- Isabelle is in principle a reactive
2.704 +system.
2.705 +There are few exceptions to the document model, for instance, when Sledgehammer
2.706 +\cite{sledgehammer-tutorial} finds intermediate proof-steps on request and
2.707 +metis \footnote{https://isabelle.in.tum.de/library/HOL/HOL/Metis.html}
2.708 +displays the respective proof steps.
2.709 +
2.710 +\sisac{}, in contrary, is designed as a tutoring system, where partners
2.711 +construct a \texttt{Specification} and a \texttt{Solution} in cooperation,
2.712 +where the user can propose a step while the system checks it and where the
2.713 +student can request help such that the system can propose a step as well.
2.714 +Since here psychology of learning is involved,
2.715 +a ``user guide'' component shall be involved in the future, and a ``user model''
2.716 +shall provide personalisation. \sisac's original architecture placed
2.717 +the components at the center of the system. But now \sisac{} is being embedded in
2.718 +Isabelle and Isabelle/PIDE is already highly elaborated --- where will be the place for
2.719 +these components in Isabelle? This is one of the major open questions
2.720 +for \S\ref{sect:implementation}.
2.721 +
2.722 +
2.723 +\subsection{Automated Specifications} \label{ssec:auto-spec}
2.724 +%------------------------------------------------------------------------------
2.725 +Sometimes a user might not be interested in specification. For instance, when
2.726 +solving an equation, the type of the problem and the respective
2.727 +\texttt{Model\_Pattern.T} are clear, and only the hierarchy of problem types
2.728 +would have to be searched for the appropriate type.
2.729 +
2.730 +
2.731 +
2.732 \<close>
2.733
2.734 (*<*)
2.735 end
2.736 -(*>*)
2.737 \ No newline at end of file
2.738 +(*>*)
3.1 Binary file src/Tools/isac/Doc/Specify_Phase/document/Screenshot-problemdef-running-expl.png has changed
4.1 Binary file src/Tools/isac/Doc/Specify_Phase/document/coil-kernel-uv.png has changed
5.1 --- a/src/Tools/isac/Doc/Specify_Phase/document/root.bib Sat Dec 30 16:49:50 2023 +0100
5.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/root.bib Sat Dec 30 17:52:03 2023 +0100
5.3 @@ -1,11 +1,233 @@
5.4 -@TechReport{isac:all,
5.5 - author = {\isac{}- Team},
5.6 - title = {\isac{} -- User Requirements Document, Software Requirements Document,
5.7 - Architectural Design Document, Software Design Document, Use Cases, Test Cases},
5.8 - institution = {Institute for Softwaretechnology, University of Technology},
5.9 - year = {2002},
5.10 - note = {\url{https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf}}
5.11 +@InProceedings{gdaroczy-EP-13,
5.12 + author = {Gabriella Dar\'{o}czy and Walther Neuper},
5.13 + title = {Error-Patterns within ``Next-Step-Guidance'' in {TP}-based Educational Systems},
5.14 + booktitle = {eJMT, the Electronic Journal of Mathematics \& Technology},
5.15 + year = {2013},
5.16 + volume = {7},
5.17 + pages = {175-194},
5.18 + month = {February},
5.19 + note = {Special Issue ``TP-based Systems and Education''},
5.20 + url = {https://php.radford.edu/~ejmt/ContentIndex.php\#v7n2}
5.21 }
5.22 +@TechReport{bb-ChatCPT-2023,
5.23 + author = {Buchberger, Bruno},
5.24 + title = {Is {ChatGPT} Smarter Than Master’s Applicants?},
5.25 + institution = {Research Institute for Symbolic Computation (RISC),
5.26 + Johannes Kepler University},
5.27 + year = {2023},
5.28 + type = {RISC Report Series},
5.29 + number = {23-04},
5.30 + address = {Linz, Austria},
5.31 + month = {January},
5.32 + url = {https://www3.risc.jku.at/publications/download/risc_6684/23-04.pdf}
5.33 +}
5.34 +
5.35 +@InProceedings{jamnik-2023.2,
5.36 + author = {Jamnik, Mateja},
5.37 + title = {{How Can We Make Trustworthy AI?}},
5.38 + booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
5.39 + pages = {2:1--2:1},
5.40 + series = {Leibniz International Proceedings in Informatics (LIPIcs)},
5.41 + ISBN = {978-3-95977-277-8},
5.42 + ISSN = {1868-8969},
5.43 + year = {2023},
5.44 + volume = {260},
5.45 + editor = {Gaboardi, Marco and van Raamsdonk, Femke},
5.46 + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
5.47 + address = {Dagstuhl, Germany},
5.48 + URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.2},
5.49 + URN = {urn:nbn:de:0030-drops-179869},
5.50 + doi = {10.4230/LIPIcs.FSCD.2023.2},
5.51 + annote = {Keywords: AI, human-centric computing, knowledge representation, reasoning, machine learning}
5.52 +}
5.53 +@InProceedings{benzmuller-2021.7,
5.54 + author = {Benzm\"{u}ller, Christoph and Fuenmayor, David},
5.55 + title = {{Value-Oriented Legal Argumentation in Isabelle/HOL}},
5.56 + booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
5.57 + pages = {7:1--7:20},
5.58 + series = {Leibniz International Proceedings in Informatics (LIPIcs)},
5.59 + ISBN = {978-3-95977-188-7},
5.60 + ISSN = {1868-8969},
5.61 + year = {2021},
5.62 + volume = {193},
5.63 + editor = {Cohen, Liron and Kaliszyk, Cezary},
5.64 + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
5.65 + address = {Dagstuhl, Germany},
5.66 + URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.7},
5.67 + URN = {urn:nbn:de:0030-drops-139028},
5.68 + doi = {10.4230/LIPIcs.ITP.2021.7},
5.69 + annote = {Keywords: Higher order logic, preference logic, shallow embedding, legal reasoning}
5.70 +}
5.71 +@MastersThesis{fkober-bakk,
5.72 + author = {Franz Kober},
5.73 + title = {Logging of High-Level Steps in a Mechanized Math Assistant},
5.74 + school = {IICM, Graz University of Technology},
5.75 + year = {2012},
5.76 + note = {\url{https://static.miraheze.org/isacwiki/e/e6/Fkober_bakk.pdf}}
5.77 +}
5.78 +@Inproceedings{EPTCS79.9,
5.79 + author = {Makarius Wenzel and
5.80 + Burkhart Wolff},
5.81 + editor = {Pedro Quaresma and
5.82 + Ralph{-}Johan Back},
5.83 + title = {Isabelle/PIDE as Platform for Educational Tools},
5.84 + booktitle = {Proceedings First Workshop on {CTP} Components for Educational Software,
5.85 + THedu'11, Wroclaw, Poland, 31th July 2011},
5.86 + series = {{EPTCS}},
5.87 + volume = {79},
5.88 + pages = {143--153},
5.89 + year = {2011},
5.90 + url = {https://doi.org/10.4204/EPTCS.79.9},
5.91 + doi = {10.4204/EPTCS.79.9},
5.92 + timestamp = {Mon, 22 Nov 2021 15:31:41 +0100},
5.93 + biburl = {https://dblp.org/rec/journals/corr/abs-1202-4835.bib},
5.94 + bibsource = {dblp computer science bibliography, https://dblp.org}
5.95 +}
5.96 +@Article{LCF-to-Isabelle-HOL:2019,
5.97 + author = {Lawrence C. Paulson and
5.98 + Tobias Nipkow and
5.99 + Makarius Wenzel},
5.100 + title = {From {LCF} to {Isabelle/HOL}},
5.101 + journal = {Formal Aspects of Computing},
5.102 + volume = {31},
5.103 + pages = {675--698},
5.104 + year = {2019},
5.105 + month = {September},
5.106 + note = {Springer, London},
5.107 + url = {https://doi.org/10.1007/s00165-019-00492-1},
5.108 +}
5.109 +@Book{gries,
5.110 + author = {Gries, David},
5.111 + title = {The science of programming},
5.112 + publisher = {Springer-Verlag},
5.113 + year = {1981},
5.114 + series = {Texts and monographs in computer science},
5.115 + doi={10.1007/978-1-4612-5983-1}
5.116 +}
5.117 +@Inproceedings{EPTCS290.6,
5.118 + author = {Neuper, Walther},
5.119 + year = {2019},
5.120 + title = {Technologies for ``Complete, Transparent \& Interactive Models of Math'' in Education},
5.121 + editor = {Quaresma, Pedro and Neuper, Walther},
5.122 + booktitle = {{\rm Proceedings 7th International Workshop on}
5.123 + Theorem proving components for Educational software,
5.124 + {\rm Oxford, United Kingdom, 18 july 2018}},
5.125 + series = {Electronic Proceedings in Theoretical Computer Science},
5.126 + volume = {290},
5.127 + publisher = {Open Publishing Association},
5.128 + pages = {76-95},
5.129 + doi = {10.4204/EPTCS.290.6},
5.130 + note = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?thedu18.6}}
5.131 +}
5.132 +@BOOK{Back1998,
5.133 + title = {Refinement Calculus: A Systematic Introduction},
5.134 + publisher = {Springer-Verlag},
5.135 + year = {1998},
5.136 + author = {Back, Ralph-Johan and von Wright, Joakim},
5.137 + note = {Graduate Texts in Computer Science},
5.138 + project = {refinement}
5.139 +}
5.140 +@Misc{sledgehammer-tutorial,
5.141 + author = {Jasmin C.Blanchette},
5.142 + title = {{Hammering Away. A User's Guide to Sledgehammer for Isabelle/HOL}},
5.143 + howpublished = {contained in the Isabelle distribution},
5.144 + year = {},
5.145 + url = {http://isabelle.in.tum.de/doc/sledgehammer.pdf}
5.146 +}
5.147 +@TechReport{imst-htl06,
5.148 + author = {Neuper, Walther and others},
5.149 + title = {{Angewandte Mathematik und Fachtheorie}},
5.150 + institution = {IMST -- Innovationen Machen Schulen Top!},
5.151 + year = {2006},
5.152 + number = {357},
5.153 + address = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
5.154 + url = {http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte\_Mathematik\_und\_Fachtheorie},
5.155 + note = {\url{http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte\_Mathematik\_und\_Fachtheorie}}
5.156 +}
5.157 +@TechReport{imst-htl07,
5.158 + author = {Neuper, Walther and Christian D\"urnsteiner},
5.159 + title = {{Angewandte Mathematik und Fachtheorie mithilfe adaptierter Basis-Software}},
5.160 + institution = {IMST -- Innovationen Machen Schulen Top!},
5.161 + year = {2007},
5.162 + number = {683},
5.163 + address = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
5.164 + url = {https://www.imst.ac.at/imst-wiki/images/f/f9/683_Kurzfassung_Neuper.pdf},
5.165 + note = {\url{https://www.imst.ac.at/imst-wiki/images/f/f9/683_Kurzfassung_Neuper.pdf}}
5.166 +}
5.167 +@TechReport{imst-hpts08,
5.168 + author = {Neuper, Walther and Reitinger, Johannes and Angelika Gr\"undlinger},
5.169 + title = {{Begreifen und Mechanisieren beim Algebra Einstieg}},
5.170 + institution = {IMST -- Innovationen Machen Schulen Top!},
5.171 + year = {2008},
5.172 + number = {1063},
5.173 + address = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
5.174 + url = {https://www.imst.ac.at/imst-wiki/images/9/9d/1063_Langfassung_Reitinger.pdf},
5.175 + note = {\url{https://www.imst.ac.at/imst-wiki/images/9/9d/1063_Langfassung_Reitinger.pdf}}
5.176 +}
5.177 +@Book{pl:milner97,
5.178 + author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
5.179 + title = {The Definition of Standard ML (Revised)},
5.180 + publisher = {The MIT Press},
5.181 + year = 1997,
5.182 + address = {Cambridge, London},
5.183 + annote = {97bok375}
5.184 +}
5.185 +@InProceedings{wn:lucas-interp-12,
5.186 + author = "Neuper, Walther",
5.187 + year = "2012",
5.188 + title = "Automated Generation of User Guidance by Combining Computation and Deduction",
5.189 + pages = "82-101",
5.190 + doi = "10.4204/EPTCS.79.5",
5.191 + booktitle = {Electronic Proceedings in Theoretical Computer Science},
5.192 + editor = "Quaresma, Pedro and Back, Ralph-Johan",
5.193 + volume = "79",
5.194 + publisher = "Open Publishing Association",
5.195 + note = {\url{https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?THedu11.5}}
5.196 +}
5.197 +@InProceedings{wn:proto-sys,
5.198 + author = {Krempler, Alan and Neuper, Walther},
5.199 + year = {2018},
5.200 + title = {Prototyping ``Systems that Explain Themselves'' for Education},
5.201 + editor = {Quaresma, Pedro and Neuper, Walther},
5.202 + booktitle = {{\rm Proceedings 6th International Workshop on}
5.203 + Theorem proving components for Educational software,
5.204 + {\rm Gothenburg, Sweden, 6 Aug 2017}},
5.205 + series = {Electronic Proceedings in Theoretical Computer Science},
5.206 + volume = {267},
5.207 + publisher = {Open Publishing Association},
5.208 + pages = {89-107},
5.209 + doi = {10.4204/EPTCS.267.6},
5.210 + note = {\url{https://arxiv.org/abs/1803.01470v1}}
5.211 +}
5.212 +@Inproceedings{mawen-23,
5.213 + author = {Miesenberger, Klaus and Neuper, Walther and St\"oger, Bernhard and Wenzel, Makarius},
5.214 + year = {2023},
5.215 + title = {Towards an Accessible Mathematics Working Environment Based on {Isabelle/VSCode}},
5.216 + editor = {Quaresma, Pedro and Marcos, Jo{\~a}o and Neuper, Walther},
5.217 + booktitle = {{\rm Proceedings 11th International Workshop on}
5.218 + Theorem Proving Components for Educational Software,
5.219 + {\rm Haifa, Israel, 11 August 2022}},
5.220 + series = {Electronic Proceedings in Theoretical Computer Science},
5.221 + volume = {375},
5.222 + publisher = {Open Publishing Association},
5.223 + pages = {92-111},
5.224 + doi = {10.4204/EPTCS.375.8},
5.225 +}
5.226 +@misc{IsaWS-22,
5.227 + title = {Towards Accessible Formal Mathematics with \sisac{} and {Isabelle/VSCode}},
5.228 + author = {W.Neuper and B.St\"oger and M.Wenzel},
5.229 + howpublished = {Isabelle Workshop 2022 \url{https://sketis.net/isabelle/isabelle-workshop-2022}},
5.230 + year = 2022,
5.231 + note = {Accessed: 202-10-13}
5.232 +}
5.233 +@inproceedings{Isabelle/Naproce,
5.234 + author = {De Lon, Adrian and Koepke, Peter and Lorenzen, Anton and Marti, Adrian and Sch\"utz, Marcel and Wenzel, Makarius},
5.235 + title = {The {I}sabelle/{N}aproche natural language proof assistant (system description)},
5.236 + booktitle = { 28th International Conference on Automated Deduction (CADE 28)},
5.237 + series = {Lecture Notes in Computer Science},
5.238 + year = {2021},
5.239 + publisher = {Springer-Verlag}
5.240 +}
5.241 @TECHREPORT{Back-SD09,
5.242 author = {Back, Ralph-Johan},
5.243 title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},
5.244 @@ -16,25 +238,44 @@
5.245 address = {Turku, Finland},
5.246 month = {July}
5.247 }
5.248 -@Book{gries,
5.249 - author = {Gries, David},
5.250 - title = {The science of programming},
5.251 - publisher = {Springer-Verlag},
5.252 - year = {1981},
5.253 - series = {Texts and monographs in computer science}
5.254 +@InProceedings{wn:lucin-thedu20,
5.255 + author = {Walther Neuper},
5.256 + title = {Lucas-Interpretation on {I}sabelle's Functions},
5.257 + booktitle = { Proceedings 9th International Workshop on Theorem Proving Components for Educational Software (ThEdu'20)},
5.258 + year = {2020},
5.259 + editor = {Pedro Quaresma and Walther Neuper and João Marcos},
5.260 + number = {328},
5.261 + pages = {79–95},
5.262 + month = {30th October},
5.263 + address = {Paris, France,},
5.264 + organization = {},
5.265 + publisher = {Electronic Proceedings in Theoretical Computer Science},
5.266 + url = {https://arxiv.org/abs/2010.16016v1},
5.267 + doi = {2010.16016v1}
5.268 }
5.269 -@Inproceedings{EPTCS-wn-20,
5.270 - author = {Neuper, Walther},
5.271 - year = {2020},
5.272 - title = {Lucas-Interpretation on Isabelle's Functions},
5.273 - editor = {Quaresma, Pedro and Neuper, Walther and Marcos, Jo\~ao},
5.274 - booktitle = {{\rm Proceedings 9th International Workshop on}
5.275 - Theorem Proving Components for Educational Software,
5.276 - {\rm Paris, France, 29th June 2020}},
5.277 - series = {Electronic Proceedings in Theoretical Computer Science},
5.278 - volume = {328},
5.279 - publisher = {Open Publishing Association},
5.280 - pages = {79-95},
5.281 - doi = {10.4204/EPTCS.328.5},
5.282 - note = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?thedu2020.5}}
5.283 +@Book{fuchs:algebra-sys,
5.284 + editor = {Fuchs, Karl Josef and Plangg, Simon and Stein, Martin and Greefrath, Gilbert},
5.285 + title = {{C}omputer {A}lgebra {S}ysteme in der {L}ehrer(innen)bildung (\"uberarbeitete Neuauflage)},
5.286 + publisher = {WTM Verlag},
5.287 + year = {2020},
5.288 + address = {M\"unster}
5.289 }
5.290 +@InProceedings{wenzel:isar,
5.291 + author = {Wenzel, Markus},
5.292 + title = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
5.293 + booktitle = {Theorem Proving in Higher Order Logics},
5.294 + year = {1999},
5.295 + editor = {G. Dowek and A. Hirschowitz and C. Paulin and L. Thery},
5.296 + series = {LNCS 1690},
5.297 + organization = {12th International Conference TPHOLs'99},
5.298 + publisher = {Springer},
5.299 + note = {\url{https://doi.org/10.1007/3-540-48256-3_12}}
5.300 +}
5.301 +@TechReport{isac:all,
5.302 + author = {\isac{}- Team},
5.303 + title = {\isac{} -- User Requirements Document, Software Requirements Document, Architectural Design Document, Software Design Document, Use Cases, Test Cases},
5.304 + institution = {Institute for Softwaretechnology,
5.305 + University of Technology},
5.306 + year = {2002},
5.307 + url = {https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf}
5.308 +}
6.1 Binary file src/Tools/isac/Doc/Specify_Phase/document/specification-complete.png has changed
7.1 Binary file src/Tools/isac/Doc/Specify_Phase/document/specification-method.png has changed
8.1 Binary file src/Tools/isac/Doc/Specify_Phase/document/specification-template.png has changed
9.1 --- a/test/Tools/isac/Test_Isac.thy Sat Dec 30 16:49:50 2023 +0100
9.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Dec 30 17:52:03 2023 +0100
9.3 @@ -45,12 +45,12 @@
9.4 \<close>
9.5
9.6 theory Test_Isac
9.7 - imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
9.8 + imports "Isac.Build_Isac" (* note that imports are WITHOUT open struct ..*)
9.9 (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one
9.10 and find out, which ML_file or *.thy causes an error (might be ONLY one).
9.11 Also backup files (#* ) recognised by jEdit cause this trouble *)
9.12 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
9.13 -(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
9.14 +(** )"$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*) ( **)
9.15 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
9.16 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
9.17 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
9.18 @@ -75,12 +75,12 @@
9.19 "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
9.20 "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
9.21 "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
9.22 -(*Test_Isac.thy*)
9.23 +(*Test_Isac.thy--\*)
9.24 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
9.25 "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) (*Test_Isac_Short*)
9.26 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*Test_Isac_Short*)
9.27 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
9.28 -(*Test_Isac.thy*)
9.29 +(*Test_Isac.thy--/*)
9.30 "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
9.31
9.32 "$ISABELLE_ISAC/Doc/Lucas_Interpreter/Lucas_Interpreter" (*Test_Isac_Short*)
10.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sat Dec 30 16:49:50 2023 +0100
10.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sat Dec 30 17:52:03 2023 +0100
10.3 @@ -50,7 +50,7 @@
10.4 and find out, which ML_file or *.thy causes an error (might be ONLY one).
10.5 Also backup files (#* ) recognised by jEdit cause this trouble *)
10.6 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
10.7 -(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
10.8 +(** )"$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*) ( **)
10.9 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
10.10 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
10.11 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
10.12 @@ -75,12 +75,12 @@
10.13 "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
10.14 "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
10.15 "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
10.16 -(*Test_Isac_Short.thy* )
10.17 +(*Test_Isac_Short.thy*--\ )
10.18 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
10.19 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
10.20 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*)
10.21 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
10.22 -( *Test_Isac_Short.thy*)
10.23 +( *Test_Isac_Short.thy--/*)
10.24 "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
10.25
10.26 (*"$ISABELLE_ISAC/Doc/Lucas_Interpreter/Lucas_Interpreter" Test_Isac_Short*)
