Database Theory in Action: Learning Logical Modelling with Iltis

Modelling data and knowledge with mathematical formalisms and subsequently attacking the underlying problems with rigorous methods is an essential part of computer science education at the university level [6, 3]. This is taught, for instance, in introductory courses on Databases (where designing database schemata and querying data with query languages is an important part) and Logic for computer science (where formalizing knowledge with logical formulas and inference mechanisms play an important role).

Based on our recent work [7], we report on how learning to model natural language statements in first-order logic is supported by the Iltis educational support system [11, 4]. As first-order logic plays an important role in database theory research, we hope that our system is helpful for members of the community who teach foundations of logic. The connection between first-order logic and core-SQL (see, e.g, [1]) may allow to transfer our insights to educational support for learning schema design and SQL.

Figure 1 depicts an exercise on first-order logic in the Iltis system²²2We invite interested readers to try this exercise in Iltis: [5] that students can typically solve after an introductory course on logic by executing the following steps:

Step 1:

Design a suitable vocabulary to describe a real world scenario by identifying suitable relation and function symbols with their intended meaning (task on the left).

Step 2:

Describe the scenario by logical formulas over this vocabulary (task on the right).

Step 3:

Transform formulas into an adequate, more simple form.

Step 4:

Infer new knowledge using an inference mechanism (e.g. resolution).

Technological support for Steps 2 – 4 has been present in state-of-the-art systems. We therefore focus on how we integrated Step 1 into the Iltis educational support system.

When students design a first-order vocabulary with the intention of writing formulas, they must say (i) which symbols they want to include, and (ii) which meaning the symbols shall have. An educational task that allows to specify a vocabulary must then check student attempts for correctness. If an attempt is not correct, it must provide feedback; if it is correct, the vocabulary can subsequently be used in follow-up tasks (compare Figure 1).

For checking these conditions automatically, an instructor needs to specify (1) which symbols can in principal be used, and (2) which subsets of symbols constitute solutions. More formally, a solution space $(𝒱,𝒮)$ consists of

• $\mathrm{■}$

  potential vocabulary symbols $v^{\ast }=(n^{\ast },D^{\ast })\in 𝒱$ with a name $n^{\ast }$ and a set $D^{\ast }=\{d_1^{\ast },d_2^{\ast },\mathrm{\dots }\}$ of natural language descriptions;

• $\mathrm{■}$

  a solution set $𝒮\subseteq 2^{𝒱}$ of subsets of symbols that constitute solutions.

Scenarios can often be modelled with many different vocabularies, yet there is often a “canonical vocabulary” from which all other vocabularies can be derived by small modifications. Examples of such modifications are that (i) constant symbols can also be modelled by unary relation symbols; (ii) $k$-ary function symbols can be modelled by $(k+1)$-ary relation symbols; and (iii) for modelling $k$ types of elements in a domain one can use either $k$ or $k-1$ unary relation symbols. In order to simplify the specification of the solution set $𝒮$, our framework allows to specify proper solutions using Boolean formulas over potential vocabulary symbols. Such a formula, for instance, can state that a unary function symbol $f$ or its corresponding binary relation symbol $F$ must be included.

Our framework, when given a student attempt $V$ containing vocabulary symbols $v=(n,d)$, works in two phases:

Mapping a symbol $v=(n,d)$ from a student attempt into the solution space requires to determine whether, and to which degree, the description $d$ corresponds to natural language descriptions of symbols in the solution space. This essentially boils down to the NLP task of determining the (semantic) similarity of pairs of strings. For first-order vocabulary symbols, it is slightly more intricate as descriptions may refer to parameters such as in Example 1. For reasons of resource efficiency and data sovereignty, instead of using LLMs, we use smaller similarity models that we fine-tuned with data sets specifically aimed at the respective assignment. Due to the lack of fine-tuning data at the time of implementation, we generated data sets for fine-tuning using a grammar-based approach that allowed us to compactly represent many different (artificial) student descriptions of different “quality”.

We summarized our article [7] and reported how the Iltis educational system integrates educational tasks for modelling with first-order logic. The full framework is described, implemented, and evaluated in that article. These educational tasks have been used in introductory logic courses for computer science students at Ruhr University Bochum and TU Dortmund University with $>300$ students each.