We are interested in automatizing reasoning with and about study regulations, catering to various stakeholders, ranging from administrators, over faculty, to students at diferent stages. Our work builds on an extensive analysis of various study programs at the University of Potsdam. The conceptualization of the underlying principles provides us with a formal account of study regulations. In particular, the formalization reveals the properties of admissible study plans. With these at end, we propose an encoding of study regulations in Answer Set Programming that produces corresponding study plans. Finally, we show how this approach can be extended to a generic user interface for exploring study plans.
students to earn a degree. This involves diferent stakeholders: faculty members designing study programs, administrative and legal staf warranting criteria, like studyability, faculty members teaching the corresponding programs as well as supervising their execution on examination boards, study advisors consulting students, and of course, students studying accordingly.
are usually rather sparse and leave many aspects to the commonsense of the respective users.
instance, often study regulations leave open minor dependencies among modules. Sometimes associated courses overlap and certain modules cannot be taken in the same semester. And ifnally, studying happens over time, students’ perspectives may change and faculty may rotate.
(KRR) makes study regulations a prime candidate for a comprehensive benchmark for KRR formalisms.
by automatizing study regulations. These users range from study administrators, over faculty in diferent functions, to prospective and advanced students. We started by analyzing more than a dozen diferent study regulations in order to identify their underlying principles. The conceptualization of the basic principles led us to a formal account of basic study regulations, presented in Section 2. For illustration, we provide the formalization of the master program Cognitive Systems. Further, more specialized concepts in other study regulations are presented in Section 3. The formalization of study regulations reveals the properties of admissible study plans. To automatize reasoning about study regulations and their study plans, we capture their properties in Answer Set Programming (ASP; [1]), a declarative problem solving paradigm, tailored for knowledge representation and reasoning. The ASP-based encoding of basic study regulations is discussed in Section 4. Moreover, we show in Section 5 how this encoding can be used together with an ASP-driven user interface to browse through study plans of given study regulations. We conclude in Section 7.
of a set of modules and a study plan is a finite sequence of semesters. More formally, given a set of modules, a study plan of semesters is a sequence ()=1 where ⊆ for
characterization of study regulations and show how they induce legal study plans.
A basic study regulation is a tuple (, , , , , , , ), where 1. is a set of modules, 2. ⊆ 2 distinguishes certain groups of modules,
4. : → {, , } assigns a regular semester to a module,
7. ⊆ 2(2 ) is a set of global constraints expressing study regulations, and 8. ⊆ 2(2 ) is a set of temporal constraints expressing study regulations. The module groups in allow us to structure the modules and to express group-wise regulations. Functions and give the credit points of a module and its turnus,1 viz. in winter, summer, or each semester (indicated by w, s, e), respectively. The elements and are partial functions delineating the number of credits obtained per module group; a specific number of credits is captured by an equal lower and upper bound. The regulation constraints in and are represented extensionally: each constraint in ∪ is represented by the sequences of sets of modules ⊆ (2 ) satisfying it. While the sets of constraints and share the same
mathematical structure, they difer in purpose and are therefore separated for clarity’s sake. expresses temporal constraints over the sequence of semesters, while does not make use of this sequential structure, and rather expresses global constraints over the entire set of modules.
all regulation constraints. More precisely, a sequence ()=1 of modules of length such that ⊆ for 1 ≤ ≤ is a study plan for (, , , , , , , ) if ()=1 ∈ ⋂︀∈∪ .
Example 1 (Cognitive systems). As an example, consider the study regulations of the master program Cognitive Systems ofered at the University of Potsdam. 2 This program ofers a combination of modules in Natural language processing, Machine learning, and Knowledge representation and reasoning.
These subjects are reflected by the three mandatory base modules, joined in in (
Finally, an internship, im, and a thesis, msc, are imposed in (16). This brings us to the temporal regulation in (20) requiring that at least 90 credits are accumulated before conducting a thesis. The temporal regulations in (18) and (19) ensure that modules are taken in the right season. And ifnally (17) makes sure that modules are chosen at most once.
Let ⊆ be some exogenous set of modules in the following example; and let stand for ⋃︀
=1 , and = { ∈ | () = } and = { ∈ | () = }. Then, the study regulations of the master program Cognitive Systems with respect to can be formalized as follows.
= ∪ ∪ ∪ ∪ {im, msc}
= {, , , , , }
= {bm | = 1..3}
= {fm | = 1..3}
= {am, | = 1..3, = 1, 2}
= ∪
= {pm | = 1..3}
= {bm ↦→ 9 | = 1..3} ∪ {am, ↦→ 6 | = 1..3, = 1, 2} ∪
(
{fm ↦→ 6 | = 1..3} ∪ {pm ↦→ 12 | = 1..3} ∪ {im ↦→ 15, msc ↦→ 30} = {bm1 ↦→ , bm2 ↦→ , bm3 ↦→ } ∪ {am, ↦→ | = 1..3, = 1, 2} ∪ {fm ↦→ | = 1..3} ∪ {pm ↦→ | = 1..3} ∪ {im ↦→ , msc ↦→ } = { ↦→ 27, ↦→ 24, ↦→ 24, ↦→ 120} = { ↦→ 27, ↦→ 24, ↦→ 24, ↦→ 120} = { {()=1 ⊆ | || ≤ 2, ∩ = }, (14) {()=1 ⊆ | () ≤ ∑︀∈∩ () ≤ ()} for all ∈ {, , , }, (15) {()=1 ⊆ | {im, msc} ⊆ } } (16) = { {()=1 ⊆ | ∩ = ∅, 1 ≤ < ≤ } (17) {()=1 ⊆ | ∩ 2 = ∅, 1 ≤ 2 ≤ , ∈ N} (18) {()=1 ⊆ | ∩ 2− 1 = ∅, 1 ≤ 2 − 1 ≤ , ∈ N} (19) {()=1 ⊆ | msc ∈ implies ∑︀1≤ < ∑︀∈ () ≥ 90, ∈ N} } (20) If the set of exogenous modules given by the examination board is, for example, = {fm1}, one admissible study plan spanning four semesters is = ()4=1, where This plan comprises 120 credits, although the load per semester varies.
For illustration, let us verify that our study plan belongs to the ones in (14) and (15) for = . Indeed constraint (14) is satisfied as we have ∩ = {fm1} = , and thus is an element of constraint (14). With regards to (15), we have
∩ = {fm1, am1,2, am2,1, am3,1} which makes us check whether our study plan satisfies
() = 24 ≤ ∑︀∈{fm1,am1,2,am2,1,am3,1} () ≤ 24 = () This is indeed the case since (fm1) + (am1,2) + (am2,1) + (am3,1) = 24. Hence, our study plan is an element of constraint (15).
behind. For instance, the number of credits per semester is left open, as is the order of the modules. The guideline is usually to take around 30 credits per semesters but this is not enforced. Similarly, basic modules in should be taken before advances ones in , again this is neither enforced nor always possible. Since these constraints are usually soft, they are left to the students and/or their study advisors.
3.1. Specialization
specialize in some area within their field of study. For example, in a biology program, one may specialize in ecology, genetics, or zoology. Each focus may contain diferent groups of modules.
of study regulations by the following concepts: • ⊆ 22 is a set of focuses, and • () and () are sets of global and temporal constraints parametrized by some focus ∈ .
constraint on the credit points for a given focus ∈ can be formalized as follows. {()=1 ⊆ | for all ∈ : ( ) ≤ ∑︀∈( ∩) () ≤ ( )} 3.2. Modules dependency
petences are required or recommended before participating in that particular module. These prerequisites are represented as hard or soft constraints, respectively. For example, the module “Introduction to Computer Science” may be required before “Data Structures”. For capturing this concept in terms of hard constraints between modules, we extend our formalization as follows: • ⊆ × relates pairs of dependent modules.
For each (1, 2) ∈ (read as 2 depends on 1), if 1 and 2 are in a study plan, the semester of 1 must be before that of 2.
{()=1 ⊆ | for all (1, 2) ∈ : 2 ∈ implies 1 ∈ , < } 3.3. Blocking modules
that block each other. For example, either version A or B of a module can be chosen, i.e. selecting the module version A blocks the choice of module version B and vice versa. For capturing this concept, we extend our formalization by the following:
• ⊆ × relates pairs of modules blocking each other.
plan but not both. We formalize the corresponding constraint by: {()=1 ⊆ | for all (1, 2) ∈ : |{1, 2} ∩ | ≤ 1} 3.4. Examination
primary examinations (e.g. passing oral exams) and secondary examinations (e.g. passing 50% of exercises). Formally: • () contains sets of possible combinations of primary examinations needed to accomplish module ∈ , and • () contains secondary examinations needed to accomplish module ∈ . Let ()=1 be a sequence of examinations of length such that ⊆ ⋃︀ ∈ ∈()
∪ ⋃︀∈ () for 1 ≤ ≤ .
Each is a set of examinations achieved at semester .
apply for a primary examination of the same module or to complete the module itself. Once a secondary examination is accomplished it persists. Finishing some primary examination is a requirement of a module to get completed. A module is accomplished as soon as all required examinations are satisfied.
our formalization by the following:
• () ⊆ () × () relates pairs of dependent examinations.
We formalize dependencies among examinations and completion of a module, respectively, by: {()=1 ⊆ | for each ∈ and each (, ) ∈ () : ⊆ ⋃︀ = implies ⋃︀(′,)∈(){′} ⊆ ⋃︀ =1 , 1 ≤ ≤ } {()=1 ⊆ | for each ∈ there exists an ∈ () : () ∪ ⊆ ⋃︀ =1 }
The formalization of the following refinements is left to the future and needed to link examinations to courses. A module defines at least one eligible teaching format for each secondary examination, e.g. exercise, lecture, seminar, tutorial, project, internship, colloquia, etc. In practice, one or more examinations of at least one module is linked to a course with a corresponding teaching format. Each student has three attempts to pass primary examination of a module. If all three attempts are failed, the module cannot be completed.
plans. As usual, this is divided into two parts: a specific instance and a general encoding.
uses the same symbols as before for sets and functions, but always in lowercase, to adapt to the conventions of ASP. For example, the sets , and are denoted by the terms s, s(i) and m(w), respectively. In what follows, we often use the logic programming notation to refer to those sets and functions.
Listing 1 shows the first part of the instance cogsys.lp for the Cognitive Systems master, that specifies the sets and functions of the study plan. Sets are defined using atoms of the form in(e,a) that represent that the element e belongs to the set a. For example, the atom in(bm1,b) expresses that bm1 ∈ b. Functions are defined similarly, using atoms of the form map(f,e,v) that represent that the value of the function f applied to the element e is v. For example, map(c,bm1,9) expresses that c(bm1) = 9. To define the facts more compactly, we make extensive use of pooling using the operator ‘;’. For example, the three facts in(bm1,b)., in(bm2,b)., and in(bm3,b). defining the set b are captured by the single rule in((bm1;bm2;bm3),b). in Line 2. 1 % b, f, a, o and p 2 in (( bm1 ; bm2 ; bm3 ) ,b ). 3 in (( fm1 ; fm2 ; fm3 ) ,f ). 4 in (( am11 ; am12 ; am21 ) ,a ). 5 in (( am22 ; am31 ; am32 ) ,a ). 6 in ( E,o ) :- in ( E, ( f ; a )). 7 in (( pm1 ; pm2 ; pm3 ) ,p ). 8 10 % m 11 in ( E,m ) :- in ( E, ( b ; f ; a ; p )). 12 in (( im ; msc ) ,m ). 13 14 15 % e 16 in ( fm1,e ).
The definitions of the constraints in (14)-(20) provide the conditions that every study plan ()=1 ⊆ must satisfy. These conditions usually refer to operations over sets, that we represent in ASP using prefix notation. For example, the condition of (14) refers to the intersection of the sets and , that is denoted in the logic program by the term int(s,f). Other terms can be used to denote the union, substraction and complement of sets. The regulation constraints could in principle be very diverse, but in our investigation of various study regulations we have found that they can be captured by a few types of general constraints, that we represent in ASP by diferent predicates. The general encoding gives their semantics, while the specific instance of each study regulation provides facts over those predicates to represent the corresponding constraints. Listing 2 shows the second part of our example instance, that specifies the constraints of the Cognitive Systems master. It uses atoms of the following form, with the associated meaning (where A and B denote sets, F denotes a function, and L and U are integers): • empty(A) means that A = ∅, • equal(A,B) means that A = B, • subseteq(A,B) means that A ⊆ B, • card(A,leq,U) means that |A| ≤ U, • sum(A,F,bw,(L,U)) means that L≤ ∑︀∈AF() ≤ U, and • sum(A,F,geq,L) means that L≤ ∑︀∈AF().
The general encoding includes more predicates to represent other relations among sets, like proper subset or superset, and it also allows other types of comparisons within atoms of the predicates card/3 and sum/4. Using these predicates, the global constraints (14)-(16) are captured in Lines 23-25. The first constraint consists of two conditions, and this is accordingly represented by two facts. Line 24 uses pooling to refer to all the sets in {b, o, p, m}, and atoms over map/3 to capture the values L and U of the functions l and u applied to those sets. The last rule of the block defines a new set gc3 that consists of im and msc, and compares it via subseteq with s. Temporal constraints are represented in Lines 28 to 31. The first three use atoms of the predicate empty/1 that refer to m(w), m(s), and the specific sets of modules s(i) of each semester i. The last one defines the set tc4 that consists of msc, applies to it a new kind of temporal operator called before, and uses the resulting term in an atom of predicate sum/4.
element of tc4; in this case, before the module msc. Using our previous mathematical notation, the set before(tc4) is { ∈ | ∈ and there is some ′ ∈ tc4 ∩ such that < }.
The general encoding includes other similar operators like after or between. 22 % global constraints 23 card ( e,leq,2 ). equal ( int ( s,f ) ,e ). 24 sum ( int ( H,s ) ,c,bw, ( L,U )) :- H = ( b ; o ; p ; m ) , map ( l,H,L ) , map ( u,H,U ). 25 in ( im,gc3 ). in ( msc,gc3 ). subseteq ( gc3,s ). 27 % temporal constraints 28 empty ( int ( s ( I ) ,s ( J ))) :- I = 1.. n, J = 1.. n, I < J . 29 empty ( int ( m ( w ) ,s (2* K ))) :- K = 1.. n, 1 <= 2* K, 2* K <= n . 30 empty ( int ( m ( s ) ,s (2* K -1))) :- K = 1.. n, 1 <= 2* K -1 , 2* K -1 <= n . 31 in ( msc,tc4 ). sum ( before ( tc4 ) ,c,geq,90 ).
Listing 3 shows the general encoding in encoding.lp. It takes as input the constant n that
gives the length of the study plan. This constant is used by the choice rule in Line 2 to generate
the possible study plans, represented by the sets s(i) for i between 1 and n. Then, Line 5 defines
the set s as the union of all s(i)’s, and Line 8 defines the sets m(w) and m(s). After this, Lines
1120 handle the additional sets that may occur in the constraints. The first block of rules identifies
the sets that occur as arguments in the constraints. Then, the rules in Lines 16 and 17 recursively
look for the sets occurring inside the operators int and before. The encoding contains other
similar rules for the other operators, but we do not show them here. Once all the new sets have
been identified, additional rules provide their definition. Line 19 defines the intersection of two
sets, and Line 20 defines the modules occurring before some module of another set. The complete
encoding includes further rules for the other operators. The next part of the encoding, in Lines
2333, enforces the constraints. The first ones about empty/1, subseteq/2 and equal/2, use the
predicate in/2 to eliminate the cases that are not consistent with the constraints, while those
about card/3 and sum/4 rely on cardinality and aggregate atoms for that task. For example, the
condition |A| ≤ U for card(A,leq,U) is captured by the cardinality atom { in(E,A) } U,
and the condition L≤ ∑︀∈AF() ≤ U for sum(A,F,bw,(L,U)) is captured by the aggregate
atom L #sum{ V,E : in(E,A), map(F,E,V) } U. Finally, the last block of statements in
Lines 36 and 37 displays the sets s(i).
1 % generate
2 { in ( E,s ( I )) } :- in ( E,m ) , I =1.. n .
4 % s = s (
We can now run the ASP solver clingo with the instance for the Cognitive Systems master and the general encoding. For n=4 we obtain, among others, an answer set that corresponds to the admissible study plan of Example 1: clingo -c n=4 cogsys.lp encoding.lp ...
Answer: 1 (bm1,1) (bm3,1) (fm1,1) (am12,1) (bm2,2) (am21,2) (pm1,2) (im,3) (am31,3) (pm3,3) (msc,4)
in accordance with study regulations. The UI allows users to add or remove modules within a semester and iterate through diferent study plan configurations based on the selected modules.
This prototype was built using the system clinguin 4 that defines the UI by a logic program that interacts continuously with clingo. Clinguin employs a Client-Server architecture, where communication occurs via an HTTP protocol using JSON. In essence, the server is responsible for executing clingo and computing the information required to define the UI, namely a uistate. This process occurs in two distinct steps. Firstly, the domain-state is computed using the domain-specific encodings (domain files) described in Section 4. This domain-state is made out of facts that diferentiate between user-selected atoms, potential selections, and inferred atoms.
style, and functionality of the interface, collectively referred to as the ui-state.
follows. The server is started by providing the domain files cogsys.lp and encoding.lp, as well as the UI file ui.lp (Listing 4) as command-line arguments:
clinguin server --domain-files cogsys.lp encoding.lp --ui-files ui.lp -c n=4 When the client is launched, it requests the ui-state from the server. Upon receiving the ui-state the client utilizes tkinter 5 to render the corresponding UI. Subsequent user interactions with the UI generate new requests to the server, providing information about the selected policy.
the next solution. Once the server has completed the policy, it returns the updated ui-state to the client to be rendered.
The detailed workflow of the server is as follows: it begins by creating a clingo control object using the given domain files ( cogsys.lp and encoding.lp) and grounding the program. It then performs three diferent solve calls to find the brave consequences (atoms considered as "possible"), cautious consequences (atoms considered as "required"), and the first model. These outputs are combined to represent the domain-state, with the brave and cautious consequences appearing in predicates _b and _c, respectively. To achieve interactivity and handle changes 4https://github.com/potassco/clinguin 5https://docs.python.org/3/library/tkinter.html efectively, this control object utilizes multi-shot solving [ 2], which allows for the continuous solving of logic programs that undergo frequent changes. In clingo, this capability is facilitated through its API, enabling the implementation of reactive procedures involving grounding and solving. In the context of interactivity, this allows us to represent the user’s selections as assumptions which are interactively modified. These assumptions are passed to the solving procedure without the need for re-grounding, and amount semantically to the addition of integrity constraints. Each assumption A is represented in the domain-state through a fact _clinguin_assume(A).
Subsequently, a separate control object is employed to generate the ui-state. By using the domain-state as input, the UI encoding (ui.lp) produces a single stable model that encompasses the atoms of the ui-state. For this, predicates element/3, attribute/3 and callback/3 are used to define the layout, style and functionality of the UI, respectively. An element X of type T inside element X’ is defined by atom element(X,T,X’). The attributes of an element, such as position and style, are specified by attribute(X,K,V), where K and V denote the name and value of the attribute, respectively. The reactive part of the UI is defined by callback(X,A,P), where performing action A on element X triggers the policy P on the server. These atoms are mapped into Python classes using clorm6, a Python library that provides an Object Relational Mapping (ORM) interface to clingo.
created using the fact in Line 1 from Listing 4. For each semester I, Line 2 generates a container
for the semester column. Line 3 creates a container for the column header, header(I), which
serves as the parent for the label (Line 4) and dropdown menu (Line 5). The dropdown menu
items are defined in Lines 6 to 8. The body in these rules is activated if the atom in(E,s(I))
is part of the brave consequences, indicating that the module E could be added to semester I.
Furthermore, not _c(in(E,s(I))) ensures that the module has not been already added. This
behavior can be observed in the first image of Figure 1, where the dropdown menu for available
modules in the third semester does not include bm2 because in(bm2,s(
found in https://github.com/potassco/clinguin/tree/dev/examples/ clingo/study_regulations.
regulation problems. However, [3] presents an overview of the AIStudyBuddy project, and contains neither a formalization of study regulations nor any implementation details. Unlike this, [4] presents a web-based Decision Support System for a degree planning problem along
server’s command-line. domain-state
domain-control brave consequences cautious consequences model clinguin assume/1 clinguin browsing
ui-control ui files domain files assumptions externals
∗(multi-shot) ui-state element/3 attribute/3 callback/3 s e i c i l o p JSON
POST
Get policy action
USER Render UI
UI with a mathematical formalization. Degree requirements are mentioned but not formalized.
students in a personalized study plan generation. It aims at reducing the duration of student plans and is implemented via integer linear programming. Finally, [6] present a data-driven approach for implementing a course recommendation algorithm. A traditional collaborative ifltering algorithm is extended to consider additional course path data.
This formalization is both simple and general to capture a wide range of study regulations. We indicated how the basic formulation easily extends to more complex constructions. This will be further elaborated in future work. The identification of basic principles in study regulations also allowed us to obtain a very general ASP encoding. The building blocks of each study regulation are captured in terms of facts so that the actual encoding is also applicable to a large range of study programs. Finally, we have described an ASP-driven user interface for interactive elaboration of study plans. Again, the interface is designed in a generic way and broadly applicable. Moreover, this case study serves as a nice illustration of clinguin and how it can be used for interactive ASP applications.
sentation and reasoning techniques. Study plans have a light temporal flavor and resemble finite traces in linear temporal logic [7]. The creation of a study plans amounts to a configuration task, which also brings about interaction and explainability. Finally, we have so far only been concerned with the hard constraints emerging from study regulations but there is so much commonsense knowledge involved, like defaults, preferences, deontic laws, updates, etc.
project CAVAS+ (16DHBKI024).