Tableaunoir is an online collaborative blackboard tool with fridge magnets available in many languages. The main raison d'être of Tableaunoir is the use of fridge magnets, to make interactive animations. The tool provides magnets for teaching algorithms, automata theory and games.
Computer science class enrollments have rapidly risen in the past decade. With current class sizes, standard approaches to grading and providing personalized feedback are no longer possible and new techniques become both feasible and necessary. Here, we present the third version of Automata Tutor, a tool for helping teachers and students in large courses on automata and formal languages. The second version of Automata Tutor supported automatic grading and feedback for finite-automata constructions and has already been used by thousands of users in dozens of countries. This new version of Automata Tutor supports automated grading and feedback generation for a greatly extended variety of new problems, including problems that ask students to create regular expressions, context-free grammars, pushdown automata and Turing machines corresponding to a given description, and problems about converting between equivalent models - e.g., from regular expressions to nondeterministic finite automata.
The University of Kassel has traditionally been a stronghold for research in educational sciences and teaching methodologies. The
Theoretical Computer Science / Formal Methods group there is working on the design, development, deployment and evaluation of software
tools for learning support not restricted to areas of theoretical computer science. One of the major aspects of this program is the application of formal methods technology to automatically generate feedback that initiates the users learning process.
In this presentation we will introduce different examples of such feedback systems developed and/or currently in development for the Sequent Calculus Trainer, a tool for learning how to construct formal proofs in propositional/ first-order logic, DIMO, a tool for the support of modelling skills in propositional logic, and the grading of homework exercises on regular languages.
In particular, the feedback systems used in these tools are based on a clear identification of a rather distinct set of competencies, which we believe is beneficial for the applicability of formal methods technology and ultimately for the effectiveness of such learning tools. Furthermore, we will discuss the formal methods applied to address these competencies, their (didactical) limitations, and how the information gathered by this technology can be used to support the learning process by students in particular parts of a course.
In this presentation, we will share our experiences when moving to an online format for the award-winning lecture series Concurrent Programming at Saarland University.
The lecture explains message-passing and shared-memory programming founded in concurrency theory.
We will report how the students made use of our supporting websites and services, including a web application allowing them to develop programs and interactively explore their semantics, a novel website combining book-like explanations and definitions with interactive exercises helping students to practice and learn from live feedback, and a few other bells and whistles.
To support students practicing with performing proofs in logic, we have developed three systems: LogEx, LogAx and LogInd.
LogEx is an Intelligent Tutoring System (ITS) in which a student can
practice the rewriting of propositional logic formulae using standard equivalences
such as De Morgan's law or distribution. The LogEx domain reasoner cal-
culates feedback automatically for propositional logic expressions submitted by
students when solving an exercise. For this purpose it uses domain knowledge,
such as rewrite steps, common mistakes, and procedures for solving an exercise.
LogEx is based on the Ideas framework, which supports the development of
ITSs that automatically generate feedback and help for step-wise exercises, for
a wide range of problem domains.
The LogEx system supports three different types of exercises: rewriting a
formula in disjunctive normal form, in conjunctive normal form, and proving the
equivalence of two formulae. Students enter their solution step-wise, providing
the next step and the corresponding rule name of the step, and receive feedback
after each step. LogEx points out syntax errors, it recognizes a wrongly motivated
but correct step, and it provides informative feedback if a common mistake occurs
(a so-called buggy rule). An example of the latter might be the distribution of
a conjunction over a conjunction. Although the result is an equivalent formula,
this application of distribution is incorrect. Our aim is to let the way of working
in LogEx resemble solving exercises using pen-and-paper as much as possible.
Hence, the equivalence proof component of LogEx facilitates working in two
directions. For example, a student can start rewriting the second formula, then
switch to the first formula, and go back to the second.
In LogAx [6] a student can practice with performing Hilbert-style proposi-
tional logic proofs. LogAx oers the same type of help as LogEx: informative
feedback, layered hints, next steps and complete solutions. If suitable, a first hint in LogAx will be a reachable subgoal. LogAx uses a dialog box in which a student chooses the axiom or rule she wants to apply. The actual application of the rule is performed by LogAx. In this way, the student can concentrate on the strategy, and occurrences of syntax mistakes such as missing parentheses are minimized.
To give feedback and help, we adapt the algorithm of Bolotov, which gener-
ates natural deduction proofs, to Hilbert-style axiomatic proofs. This adaptation
can generate a proof for any provable consequence of a set of formulae, and also
complete any partial proof.
Our latest tool, LogInd, is a tutoring system for practicing the structural
induction proof technique. LogInd guides a student through an inductive proof
by explicitly asking to state and prove a base step, an induction hypothesis and
the inductive steps.
The Iltis project provides an interactive, web-based system for teaching the foundations of formal methods. It is designed to allow modular addition of educational tasks as well as to provide immediate and comprehensive feedback. Currently, exercises for various aspects of typical automated reasoning workflows for propositional logic, modal logic, and first-order logic are covered.
Recently, Iltis has reached a level of maturity where large parts of introductory logic courses can be supplemented with interactive exercises. Sample interactive course material has been designed and used in such courses with more than 200 students.
We invite all readers to give it a try!
This is joint work with Gaetano Geck, Christine Quenkert, Jonas Schmidt, Felix Tschirbs, Fabian Vehlken, and Thomas Zeume.
Hintikka's World is an online tool for teaching epistemic reasoning. The core idea of Hintikka's World is that epistemic Kripke models are shown as comics. The tool is very graphical. The user can then explore mental states of the agents by clicking on them. The tool contains many classical AI examples, such as the Sally and Anne example. They are all formalized in Dynamic epistemic logic.
We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic, automated reasoning and formal methods. NaDeA is a browser application for classical first-order logic with constants and functions. The syntax, the semantics and the inductive definition of the natural deduction proof system along with the soundness and completeness proofs are verified in Isabelle/HOL. Finished NaDeA proofs are automatically translated into the corresponding Isabelle-embedded proofs. Hundreds of computer science students have used NaDeA for course exercises and exams since 2015.
Reference: https://nadea.compute.dtu.dk/
The Incredible Proof Machine is an easy and fun to use program to conduct formal proofs. It employs a novel, intuitive proof representation based on port graphs, which is akin to, but even more natural than, natural deduction.
In this Demo, I'll give a quick intro into the web-based UI, explain some of the features and design decisions, briefly touch upon the meta-theory (which is formalized in Isabelle!), and then I am looking forward to interesting discussion.
Pravda is an online proof assistant for learning formal logic (currently natural deduction, Hilbert-style proofs and resolution). Contrary to other tools which are purely graphical, Pravda takes an opposite approach: a proof is just a text. The syntax is very simple: each line is a formula/sequent and the whole proof is thus a sequence of formulas/sequents. Pravda also display tree-form proofs, and proofs can be exported in LaTEX. The tool provides many examples. The tool is easy to extend for capturing other proof systems.
There have been several attempts at creating Intelligent Tutoring Systems for several proof methods. Nowadays such software usually can give demonstrations and in some cases finish proofs that were already started [1]. Unfortunately, these tools tend to be pretty limited when it comes to customisation options, available proof systems and overall user experience.
This project, called Larch, aims at improving these aspects of ITS. It’s an application designed in hopes of creating a middleman between the researchers trying to implement new hint generation mechanisms and users who usually are unaccustomed to the complicated notation used in formal logic and hard to use interfaces. It guides its users through a chosen proof method, laying out possible options and their consequences, it empowers students to become more proficient, all in a user-friendly way. To achieve that, techniques of gamification were incorporated into the software, along with the best UX practices. Plugin Oriented Programming paradigm was used to create a versatile system, adaptable to users’ needs. The most notable plugins created so far include: an implementation of analytic tableaux for propositional logic, sequent calculi for intuitionistic logic with loop prevention mechanism, and a script for generating TeX code.
Long-term development plans include implementing other plugins as well as measuring the effectiveness of Larch as a tutoring application for students.
[1] Cristiano Galafassi, Fabiane F.P. Galafassi, Eliseo B. Reategui, Rosa M. Vicari, EvoLogic: Intelligent Tutoring System to Teach Logic, Brazilian Conference on Intelligent Systems (Rio Grande, Brazil), (Ricardo Cerri, RonaldoC. Prati, editors), vol. 1, Springer, 2020, pp. 110–121.
mCRL2 is a formal specification language along with certain tools for formal verification using model checking. Concurrent systems and protocols can be modelled, validated and verified with the toolset. It is available for all widely used platforms from www.mcrl2.org.
Recently, we have developed a GUI which is easy for students and teachers to learn formal verification.
Via Easychair, for more detail see the call
Back to main site