=Paper=
{{Paper
|id=Vol-2531/paper11
|storemode=property
|title=Automatic Generation of Learning Assignments for Software Engineering Formalisms
|pdfUrl=https://ceur-ws.org/Vol-2531/paper11.pdf
|volume=Vol-2531
|authors=Michael Steinle,Bernd Westphal
|dblpUrl=https://dblp.org/rec/conf/seuh/SteinleW20
}}
==Automatic Generation of Learning Assignments for Software Engineering Formalisms==
https://ceur-ws.org/Vol-2531/paper11.pdf
Automatic Generation of Learning Assignments
for Software Engineering Formalisms
Michael Steinle Bernd Westphal
Department of Computer Science Department of Computer Science
Albert-Ludwigs-Universität Freiburg Albert-Ludwigs-Universität Freiburg
Freiburg, Germany Freiburg, Germany
steinlem@informatik.uni-freiburg.de westphal@informatik.uni-freiburg.de
Abstract—Creating learning or examination assignments is a languages in the context of our undergraduate introduction to
re-occurring activity in the context of teaching. In particular software engineering [4]–[6]. Creating learning assignments in
new examination assignments are often desired for each season this context is challenging because it is not always completely
of teaching a course. In our teaching, we have observed that our
creation of assignments for software engineering formalisms uses obvious that a proposed assignment is solvable. To lower
certain intuitive constraints to obtain assignments at a designated the student’s cognitive load, we also prefer to use learning
level of difficulty and, e.g., with particular properties to be assignments where a single artefact is supposed to, e.g., be
analysed in the assignment. analysed for multiple aspects. Therefore, the artefacts for our
In this work, we present an approach where we formalise learning assignments need not only be solvable but they need
our (formerly intuitive) constraints and use constraint solving
tools to automatically synthesise learning assignments that satisfy to equally well support multiple learning goals. Hence, simple
these constraints. In our approach we leverage the fact that our mutations of existing artefacts does not provide a reliable
software engineering course teaches the majority of software procedure to create new learning assignment.
description languages fully formal. That is, an artefact using When creating new assignments, e.g., to not have the same
such a software description language is then a mathematical tasks in each seasons or for exams, we observed that we can
object for which we can give precise constraints. We demonstrate
our approach on the example of learning and examination identify different levels of difficulty within the same class of
assignments for the notion of determinism on decision table and learning assignments. Furthermore, we gained the impression
discuss applications of our assignments synthesis procedure. that we can precisely characterise those classes of difficulty
using properties of the (formal) artefacts.
I. I NTRODUCTION
We propose to develop an approach to (a) formalise our
Learning assignments are, following Seel [1], selected and
understandings of didactical aspects of learning assignments
prepared learning objects with the aim to initiate, control,
on software description languages (like solvability, learning
and organise learning processes. Following Renkl [2], learning
goals, and level of difficulty) and (b) use existing procedures
assignments in this sense are used to learn and practice knowl-
and tools to automatically generate learning assignments with
edge and capabilities. Renkl observes that different learning
desired properties. In this article, we report on an investigation
assignments can lead to comparable acquisition of knowledge
of the feasibility of this approach. To this end, we have
and that ‘well meant but badly done’ stimulations for thought
developed, implemented, and evaluated a synthesis procedure
and embeddings of learning assignment into teaching contexts
for the formalism of decision tables.
can disturb the learning process. Learning assignments have
thus to focus on the knowledge or capability to learn, and be The article is structured as follows. In Section II, we illus-
designed for and embedded into the teaching context. trate our approach on the example of learning assignment for
The question what makes a learning assignment a good basic calculus. Section III recalls decision tables and gives an
learning assignment in general and how to use certain learning example of an exam task that we would like to automatically
assignments in teaching is in our perception still actively re- generate. Sections IV and V describe our synthesis procedure
searched in didactics. A requirement for most learning assign- and preliminary empirical results, Sections VI and VII discuss
ments will be that they are solvable. Another requirement is our results and related work, and Section VIII concludes.
that learning assignments match the knowledge and experience
of the learners. Advanced learners hardly benefit from easy II. A N A NALOGY: L EARNING A SSIGNMENTS FOR
learning assignments on the competence level ‘remember’ [3] A DDITION WITH C ARRY
while beginners may be frustrated by difficult assignments on In this section, we want to illustrate the proposed approach
the competence level ‘create’ [3]. on an example of learning assignments for elementary school
In this work, we consider the problem of creating learning arithmetic, namely ‘paper & pencil’ addition with carry of
assignments with the purpose of practising analysis procedures two positive decimal numbers. As a teacher, one may want
(competence level ‘apply’) for formal software specification to present learning assignments with an increasing level of
S. Krusche, S. Wagner (Hrsg.): SEUH 2020 61
Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
T : decision table r1 ··· rn
1234 123 4 12 3 4 xn · · · x1 x0
c1 description of condition c1 v1,1 ··· v1,n
+ 625 + 6 216 +1 81716 +cn+1 yncn · · · c2 y1c1 y0
1859 186 0 21 1 0 zn+1 zn · · · z1 z0 ... ... ..
.
..
.
..
.
(a) (b) (c) (d) cm description of condition cm vm,1 ··· vm,n
a1 description of action a1 w1,1 ··· w1,n
TABLE I: Addition with carry can be simple, e.g. (a), inter- .
..
.
..
.
.. .. .
..
.
mediate, e.g. (b), or advanced, e.g. (c). Case (d) provides an ak description of action ak wk,1 ··· wk,n
abstract formal view on the task of adding two numbers.
Fig. 1: Concrete syntax of decision tables.
difficulty to let pupils practice the routine of ‘paper & pencil’
addition without carry before moving to the general case, and of the set {−, ×, ∗}, and the bottom k entries of a rule (the
possibly in between having some learning assignment with effect) w1,i , . . . , wk,i are from the set {−, ×}. That is, ‘∗’ may
exactly one carry. So the teacher may have identified the not occur in an effect of a well-formed decision table.
following three levels of difficulty: Easy tasks where no carry The semantics of decision tables is given by a function
is needed (cf. Table Ia), intermediate level tasks where exactly F that assigns to each rule r in T a propositional logic
one carry is needed (cf. Table Ib), and the general case where formula over C and A. Given premise (v1 , . . . , vm ) and effect
one carry may cause a subsequent carry (cf. Table Ic). (w1 , . . . , wk ) of r, the semantics function is defined as
To create new learning assignments for addition, e.g., in an V V
F (r) := 1≤i≤m F (vi , ci ) ∧ 1≤j≤k F (wj , aj ) (1)
e-learning tool, the teacher could firstly formalise the addition | {z } | {z }
of two n-digit decimal numbers as shown in Table Id. The =:Fpre (r) =:Feff (r)
task of adding two numbers in decimal representation consists
where F := {(×, x) 7→ x, (−, x) 7→ ¬x, (∗, x) 7→ true}.
of two numbers x and y with their decimal representation
For a discussion of the use of this semantics in requirements
xn , . . . , x0 and yn , . . . , y0 . The first carry, caused by adding
engineering we refer the reader to [4], [5].
the least significant digits x0 and y0 , is c1 , which has value 1
We can formally define different properties of decision
if and only if x0 + y0 > 10, and value 0 otherwise.
tables that are useful in requirements engineering such as
Viewing addition tasks as mathematical objects, the teacher
completeness, consistency, existence of useless rules, etc..
could secondly precisely characterise the sets of addition tasks
For the purpose of this article it is sufficient to provide the
corresponding to the levels of difficulty described above. An
definition of (non-)determinism. A decision table T is called
easy addition task is one where all carries ci , 1 ≤ i ≤ n,
deterministic, if and only if for all different rules r1 and r2 in
have value 0. Intermediate level and general case tasks can
T , their premise formulae are (logically) disjoint, i.e. if
be characterised similarly. With this formalisation of learning
assignments and the level of difficulty, the teacher could finally ∀ r1 6= r2 ∈ T • |= ¬(Fpre (r1 ) ∧ Fpre (r2 )). (2)
use any integer constraint solver that supports addition and
comparison to obtain tasks that are, e.g., in the class of easy Intuitively, a decision table is deterministic if and only if there
tasks: We are asking for a solution to the constraint solving is no valuation of the conditions in C that satisfies the premise
problem that the open symbols xi and yi are assigned values formulae of two different rules.
between 0 and 9 (decimal digits) such that the valuation To practice the analysis of decision tables for determinism,
satisfies the constraint that all carries remain 0. Note that the learning assignments can start on the competence level of
number of digits n is a parameter of the constraint solving ‘apply’. In the course, we present a truth table-based approach
problem with which the teacher can control, e.g., the time it to decide determinism for a given decision table: For each
takes to solve a task as an additional teaching aspect. valuation of the observables in C note down which rules’
That is, we propose to formalise didactical intents on premises are satisfied. The table is deterministic if and only if
learning assignments that involve mathematical objects (such no valuation satisfies more than one rules’ premises.
as addition tasks) in form of constraints and to use appro- A proof of determinism needs an argument on the rules’
priate constraint solving techniques to automatically generate premise formulae (e.g., the truth table), while a proof of
learning assignments for a given intent. non-determinism strictly speaking only needs one valuation
III. D ECISION TABLES and the argument that this valuation satisfies the premise
formulae of two different rules. Hence the workload for a
Decision tables are a simple software engineering formalism
given deterministic table can be higher (construction of truth
that can, e.g., be used to formalise requirements [7], [8].
table) than for a given non-deterministic table (give a counter-
Formally, a decision table T is an (m + k) × n matrix with
example as explained above). Thus in the role of a teacher,
entries from the set {−, ×, ∗}. The top m rows correspond to
we often want to control whether the decision table given as
conditions c1 , . . . , cm from the set of conditions C, and the
a learning assignment is deterministic or non-deterministic.
bottom k rows to actions a1 , . . . , ak from the set of actions A,
which is disjoint from C. Columns are called rules. The top Figure 2 shows a simplified example of an exam task on
m entries of a rule (the premise) v1,i , . . . , vm,i are elements decision tables. The Subtask (1) tests that students are able
S. Krusche, S. Wagner (Hrsg.): SEUH 2020 62
T r1 r2 r3 1) Give the rule formulae for r1 , r2 , r3 . learning assignment decision table
c1 × × − specification
2) It is claimed that T is deterministic.
c2 × − ∗ (1)
Prove this claim.
c3 − × ∗ (3)
constants formulae
a1 × − − 3) Does T have a useless rule?
a2 − × − Prove your claim. (2)
model
Fig. 2: Example exercise task on decision tables.
Fig. 3: Intermediate artefacts of decision table task generation.
to use the semantics function (competence level ‘apply’). some of these further constraints at the end of this section. The
This kind of task is obviously solvable for each well-formed basic idea of our procedure to generate deterministic decision
decision table, yet to be most useful, one may wish to provide tables is to reduce the generation problem to an SMT-problem.
a table that comprises all possible entries. Subtask (2) tests SAT modulo theory (SMT) is a natural problem domain due
competences in applying a particular proof strategy for a to the logical nature of the decision table semantics.
particular decision table property. This subtask is only solvable Finite sets C and A of conditions and actions and a
(or at least not strongly confusing) if the considered decision number n ∈ N0 of rules constitute the learning assignment
table has the claimed property. Subtask (3) tests competences specification (cf. Figure 3). In Step (1), we define the signature
on analysing a decision table for whether it has a certain of the SMT-problem as a set of constants, one constant per
property such as useless rules (hence touching the competence decision table cell. Over this signature, we generate formulae
level ‘analyse’). Depending on the correct answer, different that, e.g., specify the allowed content of decision table cells
proof strategies apply that may need a significantly different and also the determinism property. In Step (2), an SMT-solver
amount of time to solve. One may aim at a decision table for generates a model, i.e., an interpretation of the signature such
which Subtasks (2) and (3) need different proof strategies so to that the considered formulae hold under this interpretation (if
test both and to limit the necessary effort. Note that using only and only if a deterministic decision table of the desired size
one decision table lowers the cognitive load for the learners exists). In Step (3), we interpret the model as a decision table.
since only one artefact needs to be read and the learners can To obtain a second, different deterministic decision table, the
concentrate on the analysis tasks as such. model from the previous run can be encoded as an additional
Creating learning assignments as shown in Figure 2 is formula. Then, taking Step (1) again, we obtain a model that
difficult because multiple constraints need to be considered encodes a different deterministic decision table (if and only if
together. A change in one cell of the decision table may a second decision table of the desired form exists).
unintentionally render the table non-deterministic, or make the The idea of the encoding is as follows: For each premise
analysis for determinism too easy (for example by having two cell of the desired decision table, there is one constant in the
identical rules). To simplify the process of creating learning signature that can take values ‘×’, ‘−’, or ‘∗’, and similarly
assignments or exam tasks on decision tables, we propose for each effect cell, then with possible values ‘×’ or ‘−’. So
to exploit the fact that decision tables are introduced as to obtain a table over m conditions and k actions with n rules
mathematical objects in our course. Properties of decision (cf. Figure 1), we would have constants v1,1 , . . . , vm,n and
tables, such as determinism, are formally defined and thus can w1,1 , . . . , wk,n . Now any model of the trivial formula ‘true’
be used as constraints in a synthesis procedure. In addition, we as returned by an SMT-solver is already an encoding of a well-
propose to formalise our didactical understanding of classes of formed decision table: The entry of cell, e.g., vi,j takes the
learning assignments on decision tables. For example, that an interpretation of the constant vi,j , which is ‘×’, ‘−’, or ‘∗’.
analysis for non-determinism is trivial if there are two identical Providing a constraint that corresponds to determinism is
rules in the table. Other examples aim at the corner cases of a bit more involved. Firstly, the definition of determinism
the definition of determinism from the course and we may (cf. (2)) refers to a fixed decision table with fixed premise
want to leave out these cases in beginner’s exercises. The task formulae. For decision table generation, we need a formula
to create, e.g., a complete decision table of a particular size that refers to the decision table as encoded by the constants
then reduces to a mathematical constraint solving problem. vi,j and wi,j . Secondly, the definition of determinism refers
to validity of propositional formulae by using the validity
IV. G ENERATING L EARNING A SSIGNMENTS ON
operator ‘|=’ (read: for each valuation of the conditions in C,
D ETERMINISTIC D ECISION TABLES
the negation of two different rules’ premise formula evaluates
In the following, we outline a procedure to generate de- to true). Such a validity operator is usually not directly
terministic decision tables of a specified size. We focus available in SMT-solvers.
on deterministic decision tables. Non-deterministic decision We observe that the premise formula of a rule r in a decision
tables are the dual case (we negate one of the learning table is obtained using the helper function F . Function F
assignment creation constraints), yet to be useful learning basically says, that a given valuation σ : C → {0, 1} of the
assignments, non-deterministic decision tables need further conditions in C is enabling the i-th cell (in the row of condition
didactic constraints, e.g., on the level of difficulty. We discuss ci ) of the j-th rule if and only if this cell holds symbol ‘×’ and
S. Krusche, S. Wagner (Hrsg.): SEUH 2020 63
is elapsed time (blue); the total user time (yellow) grows
300 30
t/s t/s
faster because the underlying solver effectively uses multi-core
250 25
systems. The top graph shows the time needed to generate one
200 20 decision table of size (n+n)×n (n conditions and actions, and
150 15 n rules). For values of n up to 10, the runtime is in the order
100
9
of seconds. Hence generating decision tables for our exercises
50 5
and exams is well feasible, because our tasks usually have 3
to 5 conditions, about 3 actions, and not more than 7 rules.
2 3 4 5 6 7 8 9 10 11 12 13 n 1 5 10 15 20 N
Working on larger decision tables in ‘paper & pencil’ style is
(a) Generation of one decision (b) Generation of a new bunch of 100
table of size (n + n) × n. decision tables of size (3 + 3) × 3.
in our opinion not supporting the learning but just tedious.
One use case that we envision for our procedure is to
Fig. 4: Runtimes for two kinds of decision table generation generate bunches of decision tables as task candidates for
tasks (: user time, : elapsed time, : kernel time). the teacher to choose from. The bottom graph in Figure 4
shows that the time needed for generating bunches of 100
decision tables for n = 3 is in average about half a second. An
σ(ci ) = 1, or this cell holds symbol ‘−’ and σ(ci ) = 0, or this inspection of the bunches shows that using SMTInterpol has
cell holds symbol ‘∗’ (“don’t care”). In the SMT-encoding, the the effect that the tables in the bunches do not feel too regular
symbol in “this cell” is given by the value of constant vi,j , (i.e., not like a mere enumeration of decision tables) and that
hence the equivalence stated above corresponds to the formula we do not get too many symmetric decision tables. Still, we
Gi,j := (vi,j = × ∧ ci ) ∨ (vi,j = − ∧ ¬ci ) ∨ (vi,j = ∗) (3) plan to give teachers the possibility to refine the specification,
e.g., to limit the number of ‘∗’ symbols (the fewer ‘∗’ symbols
over a logical variable ci . Formula (3) holds if and only if the a decision table has, the more obvious the determinism).
current value of ci enables the currently considered entry of the
decision table cell as given by the interpretation of constant VI. D ISCUSSION
vi,j . A rule r is enabled by a valuation σ if and only if σ
satisfies Fpre (r), which is the case if and only if σ enables The previous sections show that it is possible to synthe-
all cells that constitute the premise of r. Hence the formula sise learning assignments for software description formalisms
Gj := G1,j ∧ · · · ∧ Gm,j corresponds to the enabledness of (viewed as mathematical objects) that satisfy certain precisely
rule rj (where the rule is given by the current interpretation stated constraints. These constraints can be very generic,
of the vi,j ). So to obtain a deterministic decision table, we in our case the full power of logic over some theory is
conjoin the overall formula available. Here we see a strong potential of our approach:
We formalise conditions that make learning assignments good
G := ∀ 1 ≤ j1 6= j2 ≤ n ∀ c1 , . . . , cm • ¬(Gj1 ∧ Gj2 ) (4)
learning assignments, relative to the teacher’s intention and the
to the SMT-problem. The particular SMT-problem is now to students’ situation in the same way as sketched for addition
provide an interpretation of the signature (i.e., the constants tasks in the introduction.
vi,j and wi,j ) such that G is satisfied. For details of the In the case of decision tables, we have for example ob-
encoding, we refer the reader to [9]. Note that all quantifiers served that the tasks that we create anew each season for the
in G (cf. (4)) range over finite domains and can hence be exercises and the exam follow certain principles. One is of
expanded into a finite conjunction. The expanded formula course the size of the tables (as already considered in our
is then treatable by efficient SMT-solvers for quantifier-free generation procedure). With non-deterministic decision tables,
theories. The unfolding grows in the number of conditions we do consider more aspects. For example, a table where
and desired rules. Yet, since we aim to create decision tables two rules are just copies of each other could be too easy
that are supposed to be solved by humans, we expect that the to analyse. We can immediately formalise that there are no
unfolding of G into a quantifier-free formula is usually still two identical rules and add that constraint to the learning
well-treatable by today’s SMT-solvers. Prelimary evaluation assignment specification. Then, our definition of determinism
results as reported below confirm our expectation. has the particularity that actions are not considered. So if
two rules can be enabled by one valuation of the conditions
V. E VALUATION and have the same effect, they are still (by definition) non-
We have implemented our approach using the API of the deterministic. A table with all different effects could be a
SMT-solver SMTInterpol [10]. We imagine to offer to teachers good choice when starting with non-deterministic tables, yet
a choice of decision tables for a given learning assignment the corner-case of overlapping premise and equivalent effect
specification, and the possibility to refine the specification, should be presented to the advanced learner. Again, we can
e.g., to limit the number of ‘∗’ symbols (the fewer ‘∗’ symbols formalise both cases as constraints. Furthermore, an analysis
a decision table has, the more obvious the determinism). for non-determinism could be too easy if there are too many
Figure 4 shows the runtime of decision table generation ‘∗’ symbols in the table, so we may want to add a constraint
using our implementation. The practically most relevant graph that limits the number of ‘∗’ symbols overall, or just per rule.
S. Krusche, S. Wagner (Hrsg.): SEUH 2020 64
The same applies to other properties of decision tables, such provide a procedure to generate problems that ask to construct
as completeness, consistency, presence of useless rules, etc.. a DFA that accepts a certain language from a set of so-called
Once we have established a set of constraints that can be seed problems. They propose a metric of difficulty based on
added to learning assignment generation runs, there are mani- number of states, depth, and number of counter-examples used
fold applications. The most obvious application is to generate by a learning algorithm.
exercises or exam tasks tailored to a particular teaching or Our approach can be seen to take one step back since we
testing goal (cf. Figure 2). It is easy to embed our decision feel that teaching of software description languages is not yet
table synthesis procedure into a tool where a teacher only as well-researched as, e.g., geometry or algebra. We put the
selects the kind of task to obtain a task statement and a teachers’ understanding of learning assignments first and want
matching decision table. We envision a tool that presents a to provide problem encodings such that teachers can formalise
selection of tasks to teachers. We feel that the teacher needs their understanding of problem classes and have complete
to decide and should not blindly rely on a tool. The experience control over generated problems.
from our experiments is that a set of 10 (or even 100) decision
VIII. C ONCLUSION
tables usually includes many examples of good exercises.
Having decision tables available in machine readable form We have presented a logic-based approach to characterise
allows us to generate much of the necessary material automat- and synthesise learning assignments for a subset of the formal
ically, including correction schemes and slides for tutorial ses- software description language of decision tables. A first eval-
sions. In tutorials that discuss non-determinism, there could be uation shows that our procedure quickly generates problems
overlays for the case with disjoint effects and the corner-case of the size needed for ‘paper & pencil’ tasks. We argue to
with equivalent effects. Further applications could be to offer put computer science teachers into a prominent position when
an e-learning tool, e.g., a website or a mobile application, that generating learning assignments: A formalisation of software
generates new learning assignments for a student-controlled engineering problems allows us teachers to formalise and
or heuristically adapted level of difficulty. Note that we want investigate our understanding of good learning assignments.
to address learning activities that focus on the formalisms Future research includes to extend the set of supported
and analysis procedures as such. To this end, it is perfectly learning assignments (also for different formalisms), and fur-
adequate that the generated decision tables do not model an ther research into the nature of instructionally good learning
existing system. In our opinion, students should not firstly assignments and their formal characterisation.
assess the pragmatics of a decision table model, or try to look R EFERENCES
out for non-determinism in their imagination of the modelled
[1] N. M. Seel, Lernaufgaben und Lernprozesse, ser. Studienbuch
system, but they should learn to rely on the purely abstract Pädagogik. Stuttgart: W. Kohlhammer, 1981.
application of analysis procedures. [2] A. Renkl, “Lernaufgaben zum Erwerb prinzipienbasierter Fertigkeiten,”
From our experience with exercises for our software en- in Lernaufgaben entwickeln, bearbeiten und überprüfen, ser. Fachdidak-
tische Forschungen, vol. 6, 2014, pp. 12–22.
gineering course, we anticipate that our approach can be [3] L. W. Anderson, D. R. Krathwohl et al., Eds., A Revision of Bloom’s
extended to class diagrams, object diagrams, OCL constraints Taxonomy of Educational Objectives. Longman, 2001.
together with class diagrams, and even Statechart-like for- [4] B. Westphal, “An undergraduate requirements engineering curriculum
with formal methods,” in REET@RE, M. Moshirpour, M. Moussavi,
malisms. It is an open research question which synthesis A. M. Grubb, S. Gregory, and B. Far, Eds. IEEE, 2018, pp. 1–10.
procedure is adequate for which formalism. [5] ——, “Formale methoden in der Softwaretechnik-Vorlesung,” in SEUH,
V. Thurner et al., Eds., vol. 2358. CEUR-WS.org, 2019, pp. 21–33.
VII. R ELATED W ORK [6] ——, “Teaching software modelling in an undergraduate introduction to
software engineering,” in EduSymp. IEEE, 2019, pp. 0–0.
The idea to generate learning assignments is not new. [7] H. Balzert, Lehrbuch der Softwaretechnik: Basiskonzepte und Require-
worksheets for elementary school arithmetic are generated ments Engineering, 3rd ed. Spektrum, 2009.
[8] ——, Lehrbuch der Softwaretechnik: Entwurf, Implementierung, Instal-
randomly (e.g., [11]) and, e.g., [12] use mutations of templates lation, Betrieb, 3rd ed. Spektrum, 2011.
for state-machine problems. Singh et al. [13] infer a set of [9] M. Steinle, “Automatische Generierung von Lernaufgaben für Entschei-
similar problems on algebraic equivalence proofs from an dungstabellen,” 2019, B. Sc. thesis, Universität Freiburg.
[10] J. Christ, J. Hoenicke, and A. Nutz, “SMTInterpol: An Interpolating
abstraction of a given problem into a so-called query, where SMT Solver,” in SPIN, ser. LNCS, A. F. Donaldson and D. Parker,
queries can also serve to give learning assignment specifica- Eds., vol. 7385. Springer, 2012, pp. 248–254.
tions. Similarly, Ahmed et al. [14] propose to abstract natural [11] mathworksheetwizard.com. (2019)
[12] D. Sadigh, S. A. Seshia, and M. Gupta, “Automating exercise generation:
deduction proofs and to then generate comparable problems. a step towards meeting the MOOC challenge for embedded systems,”
Alvin et al. [15] targets the synthesis of geometry problems in WESE, P. Marwedel, Ed. ACM, 2012, p. 2.
from an example with a set of properties to be preserved. [13] R. Singh, S. Gulwani, and S. K. Rajamani, “Automatically generating
algebra problems,” in AAAI, 2012.
They suggest that proof width and length, and the number [14] U. Z. Ahmed, S. Gulwani et al., “Automatically generating problems
of deductive steps are useful metrics to control the synthesis. and solutions for natural deduction,” in IJCAI, 2013, pp. 1968–1975.
Andersen et al. [16] propose to characterise the difficulty of [15] C. Alvin, S. Gulwani, R. Majumdar, and S. Mukhopadhyay, “Automatic
synthesis of geometry problems for an intelligent tutoring system,”
problems by the execution trace of a procedure that solves the CoRR, vol. abs/1510.08525, 2015.
problem, and to synthesise problems along such a procedure [16] E. Andersen et al., “A trace-based framework for analyzing and synthe-
to obtain a controlled learning progression. Sadigh et al. [12] sizing educational progressions,” in SIGCHI. ACM, 2013, pp. 773–782.
S. Krusche, S. Wagner (Hrsg.): SEUH 2020 65