Important learning objectives in database education are to learn how to design database schemas and how to write queries to access data stored in a database adhering to a schema. In this article we report on results from [Tristan Kneisel et al., 2025] where this learning objective is addressed for the related educational task of modelling with logical formalisms. Two key steps in logical modelling are to (a) choose a suitable vocabulary, that is, e.g., which first-order symbols to use and with which intended meaning, and then to (b) construct actual formal descriptions, i.e. first-order formulas over the chosen vocabulary. While (b) is addressed by several educational support systems for formal foundations of computer science, (a) is so far not addressed at all - likely because it involves specifying the intended meaning of symbols in natural language. We propose a conceptual framework for educational tasks where students choose a vocabulary and implement it for tasks for designing propositional and first-order vocabularies within the Iltis educational system.

First-order logic is the basis for many knowledge representation formalisms and methods. Providing technological support for learning to write first-order formulas for natural language specifications requires methods to test formulas for (non-)equivalence and to provide explanations for non-equivalence. We propose such methods based on both theoretical insights and existing tools, implement them, and report on experiments testing their effectiveness on a large educational data set with > 100.000 pairs of first-order formulas.

Explaining why and how a tree t structurally differs from another tree t^⋆ is a question that is encountered throughout computer science, including in understanding tree-structured data such as XML or JSON data. In this article, we explore how to learn explanations for structural differences between pairs of trees from sample data: suppose we are given a set {(t₁, t₁^⋆),… , (t_n, t_n^⋆)} of pairs of labelled, ordered trees; is there a small set of rules that explains the structural differences between all pairs (t_i, t_i^⋆)? This raises two research questions: (i) what is a good notion of "rule" in this context?; and (ii) how can sets of rules explaining a data set be learned algorithmically? We explore these questions from the perspective of database theory by (1) introducing a pattern-based specification language for tree transformations; (2) exploring the computational complexity of variants of the above algorithmic problem, e.g. showing NP-hardness for very restricted variants; and (3) discussing how to solve the problem for data from CS education research using SAT solvers.

Computational reductions are an important and powerful concept in computer science. However, they are difficult for many students to grasp. In this paper, we outline a concept for how the learning of reductions can be supported by educational support systems. We present an implementation of the concept within such a system, concrete web-based and interactive learning material for reductions between graph-based problems, and report on our experiences using the material in a large introductory course on theoretical computer science.

We are interested in the following validation problem for computational reductions: for algorithmic problems $P$ and $P^\star$, is a given candidate reduction indeed a reduction from $P$ to $P^\star$? Unsurprisingly, this problem is undecidable even for very restricted classes of reductions. This leads to the question: Is there a natural, expressive class of reductions for which the validation problem can be attacked algorithmically? We answer this question positively by introducing an easy-to-use graphical specification mechanism for computational reductions, called cookbook reductions. We show that cookbook reductions are sufficiently expressive to cover many classical graph reductions and expressive enough so that SAT remains NP-complete (in the presence of a linear order). Surprisingly, the validation problem is decidable for natural and expressive subclasses of cookbook reductions.

Iltis is an interactive, web-based system for teaching logic. It is designed to provide immediate and comprehensive feedback for exercises covering various aspects of the reasoning workflow. This poster presentation reports on new exercises and feedback mechanisms for modal and first-order logic.

Logic is a foundation for many modern areas of computer science. In artificial intelligence, as a basis of database query languages, as well as in formal software and hardware verification — modelling scenarios using logical formalisms and inferring new knowledge are important skills for going-to-be computer scientists.