ABSTRACT. Modern Boolean Satisfiability (SAT) solvers, based on the Conflict-Driven Clause Learning (CDCL) paradigm, achieve state-of-the-art efficiency but present a steep learning curve due to their sophisticated algorithms and highly optimized data structures. Understanding these complex mechanics and evaluating the effectiveness of problem encodings is notoriously challenging for students and emerging researchers. To ease this learning process, we introduce the Interactive SAT Tracer (SAT-IT), an open-access web environment designed to make the foundations of SAT solving highly visible and interactive. SAT-IT offers a staged pedagogical progression: from naive backtracking to DPLL and full CDCL with the two-watched literals scheme. Users can clearly inspect fundamental data structures, search space trails, and solving statistics. The tool interactive search space exploration is boosted with literal-level breakpoints for targeted inspection, alongside versatile automatic solving modes that offer both continuous real-time execution and state-based subroutine automation. Combined with a powerful ``what-if'' capability for stepping backward to explore alternative decisions, an instance manager, and an extensible architecture ready to support additional algorithms, SAT-IT serves as a practical, granular lens for experimenting with SAT solving algorithms and analysing encodings efficiency.

ABSTRACT. Logic for Fun is an online tool aimed at teaching the skill of using first order logical notation to specify problems in such a way that a model of the encoding is a solution to the problem. Older versions of the tool have been in use for many years, but the latest (2026) offers increased functionality to improve both the user experience and the process of assessing students' work. In this demonstration, we give an overview of the site and illustrate the process of using it to solve problems.

ABSTRACT. We present LogicProof, an interactive web-based theorem prover designed for educational use. The system supports natural deduction and sequent calculus for propositional and first-order logic in both classical and constructive variants. It emphasizes a modern user experience through real-time feedback and interactive visualization of proof trees. We evaluated LogicProof in a study involving 35 students. The results suggest that the system improves understanding of formal proof construction and supports student engagement with logical concepts. Compared to traditional pen-and-paper approaches, students reported faster iteration, easier error correction, and greater confidence in the correctness of their solutions. These findings indicate that LogicProof can serve as a practical supplement to existing teaching methods, particularly in supporting the learning process and reducing barriers associated with formal proof construction.

ABSTRACT. Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and ω-automata manipulation. While Spot is routinely used as a research and verification back-end, its rich visualization capabilities and Python interface also make it an attractive platform for teaching the connections between temporal logic formulas and the ω-automata that give them their semantics. This demonstration showcases two complementary, zero-install entry points into Spot that are suitable for educational settings: 1. a web application that lets students type LTL or PSL formulas and immediately see the resulting automaton, explore formula simplifications, compare formula equivalence/implication, and navigate Manna & Pnueli’s temporal hierarchy. 2. Jupyter notebooks that combine narrative explanations, live Python code, and inline automaton drawings, enabling students to experiment interactively and instructors to build assignments around concrete, executable examples. Additionally, we can discuss the use of the command-line tools of Spot to generate random examples suitable for preparing a series of exercises.

ABSTRACT. Often, the easiest way to learn something is to have to use it for a purpose. This purpose can be playful: In *Tempus fugit*, the player takes on the role of a magician who has to defeat enemies by casting spells. The applicability of spells and enemy attacks depends on the truth of formulas in linear temporal logic with past with respect to a trace that the player gradually builds. So whoever wants to save the realm from monsters has to learn to read logic formulas. This paper describes the small browser game and explains our design choices. We expose how game mechanics connect to linear temporal logic with past over finite traces, and how this can help players approach a daunting topic like formal logic. (Submitted to both Plenary demo and Shared-time demo category.)

ABSTRACT. Now pervasive in many mathematics and computer science research domains, proof assistants have recently gained importance in education, mostly during the college years. In this demo we showcase a new learning environment as a layer above the Lean proof assistant, specifically targeting high-school level proofs. Drawing inspiration from other adaptations of proof assistants for teaching, such as Lean-Verbose and Coq Waterproof, along with our own experience using proof assistants in higher education, we designed Yalep --- Yet Another Learning Environment for Proof --- a declarative controlled natural language, with a minimal number of syntactic constructions, which favors forward-chaining of facts. [Note: we also applied for a "Shared-time demo" with the same extended abstract, with a preference for a "Plenary demo" over a "Shared-time demo" if possible]

ABSTRACT. Dual submission for Plenary and shared-time demo ----- Waterproof Editor provides an educational environment specifically targeted to teaching with proof assistants or programming languages. It arose from Waterproof, educational software targeted at helping students acquire the skill of giving mathematical proofs. Its original features such as enabling rich formatting and providing clear input areas are now abstracted away in an npm package and can be used in different educational contexts. We invite interested parties to use this component in their educational software, and offer to assist with this.

ABSTRACT. The first part of this paper provides an experience report, recounting the design and long-term maintenance of the Carnap proof assistant framework used cumulatively by over 45,000 students worldwide over the last decade. We cover the good, the bad, and the ugly: what worked well, what didn't work, and what added friction to development and maintenance over time. These insights motivate a bottom-up redesign of the Carnap framework, which is the topic of the paper's second part. Briefly, the new design combines a new high-performance verifier kernel (mm0-zig) targeting Mario Carneiro's metamath zero format, and the Aufbau Bytecode Compiler, (abc), a new proof compiler that can serve as a backend for richly interactive proof-authoring experiences on the web.

ABSTRACT. Introductory courses in the formal foundations of computer science are often attended by large numbers of students from diverse backgrounds. In this talk, we will outline how this challenge can be addressed using web-based, interactive exercises provided by Iltis (https://iltis.rub.de/), a modern educational support system covering the foundations of logic, formal languages, and (parts of) complexity theory. We will give a brief introduction to Iltis and outline the research challenges and opportunities for theoretical computer science that arise in the development of such a system. This talk is based on an article that appeared in the Educational Column of the EATCS Bulletin and previous talks on the subject. We attached the article and previous slides.

ABSTRACT. The LTL Tutor is a misconception-based tutor that improves understanding of LTL. It integrates knowledge of and tooling for LTL, several years of user-studies, and concepts from education research into a seamless package.