Formal Methods Education Online: Tips, Tricks & Tools (FOMEO)

Online instruction of formal methods has gained more and more importance over the last years, including teaching of basics of logics and automata theory, formal verification, theorem proving, knowledge representation etc.
This workshop brings together instructors of formal methods as well as developers of teaching support systems for formal methods to
(a) present teaching support systems for formal methods education, and
(b) discuss experiences with and concepts for developing online courses and tools.

List of presented tools

Here is a short overview of all the presented tools.

Logic

• Name: DiMo
Area: logic
Content: editor and solver (satisfiability, validity, equivalence) for parametrized propositional formulas
Usage: by students as support for exercises on discrete modelling in propositional logic; can be used as a sat-solver interface
• Name: First-Order Logic Workbook
Area: first-order logic, semantics, formal proofs, modelling
Content: Computational notebook interface (akin to Jupyter, etc.) for designing and solving of first-order logic problem sets with formerly independent tools from our toolbox (semantic tableau editor, finite structure explorer, resolution proof editor, formalization checker [to be integrated soon]). Virtual worksheets include rich text cells with LaTeX-coded math and tool cells, which can both be rearranged and comment on. Worksheets are saved directly in a GitHub repository.
Usage: The Workbook web app requires a GitHub login. You can then create and edit the worksheets in any of your GitHub repositories. Clone our repo https://github.com/FMFI-UK-1-AIN-412/workbook-example to get started.
Tools presentation
• Name: Hintikka's World
Area: Modal logic
Content: Examples of Kripke models: muddy children, dining cryptographers problem, etc.
Usage: Explore Kripke models, model checking of formulas
• Name: Iltis
Area: Logics (in the future further fields like formal languages as well)
Content: Exercises for the complete reasoning workflow (modeling, transformation, testing for satisfiability) for propositional, modal, and partially first-order logic; some other tasks like formula evaluation, model construction, ... for these logics; atomic tasks can be combined to form larger workflows
Usage: Iltis can be freely tested under the given link; to use it in your course, please get in touch with us (e.g. via the comment functionality on our website), then you can create your own pages and publish them under a customized link
• Name: Larch
Area: Proof methods for formal logic.
Content: A prototype of an Intelligent Tutoring System that supports learning different proof methods (such as analytic tableaux or sequent calculi).
\$ analytic tableaux method for propositional logic (and more proof methods in the future). The main ideas behind the interface are: step-by-step guidance through the proof, effective hint system and engaging gamification features.
• Name: LogEx, LogAx and LogInd
Area: Logics

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 calculates 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 propositional 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 generates 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.

• Name: Natural Deduction Assistant (NaDeA)
Area: Proof systems in logic (classical first-order logic with constants and functions)
Content: Construction of formal proofs in natural deduction with automatic translation to Isabelle/HOL and feedback on proof rule applications.
Usage: Interactive web application with proofs entered using a simple point and click interface. The tool is free to use for everyone, and help and examples are available as part of the tool.
• Name: Pravda
Area: Proof systems in logic
Content: Exercices in resolution and natural deduction
Usage: Understand proof systems, write proofs
• Name: Prooffold
Area: Proofs in mathematics and theoretical computer science
Content: This tool displays proofs in a hierarchical form. By clicking on some argument, the tool shows its proof. By hovering some argument, it highlights its premisses.
Usage: This tool is used to understand the structure of a proof. It enables also to explore a long and involved proof. Typically, students may explore some proof and explain some parts of it. In the future, we may think that this tool helps to build new structured proofs.
• Name: Sequent Calculus Trainer
Area: logic
Content: constructing formal proofs in sequent calculus with automated feedback on the provability status
Usage: by students as support for exercises on proving validity of formulas in sequent calculus; helps presenting proof construction during lectures
• Name: Sequent Calculus Verifier (SeCaV)
Area: Proof systems in logic (classical first-order logic with constants and functions)
Content: Construction of formal proofs in sequent calculus with automatic translation to Isabelle/HOL and feedback on proof rule applications.
Usage: Interactive web application with proofs written in a simple textual syntax. The tool is free to use for everyone, and help and examples are available as part of the tool.
• Name: SIVA
Area: simulation and visualization of the tableau algorithm for the ALC description logic
Content: A user builds a completion tree (to prove the input consistency) step-by-step, supervised by SIVA. The main goal of SIVA is to teach the DL tableau expansion rules and to visualize the completion tree.
Usage: Define the symbols of the vocabulary, write the knowledge base, choose a decision problem to be solved, and construct a completion tree step-by-step (supervised by the app) using the tableau rules.
• Name: The Incredible Proof Machine
Area: Logic and formal proves
Content: Game-like exercises in propositional and predicate logic using natural deducation.
Usage: Novel graph-based proof representation with an interactive web- based environment.

Formal languages and methods

• Name: Automata Tutor
Area: Formal languages
Content: Exercises on DFA, NFA, RE, PDA and CFG (understanding, construction, conversions and further algorithms)
Usage: Register online - Become instructor - Create your own exercises for your course
• Name: pseuCo Book
Area: process calculi, concurrent programming
Content: explanations & interactive exercises on isomorphism, (weak) bisimilarity, observation congruence, and concurrent programming with message passing and shared memory
Usage: You can use the existing exercises in your courses
• Name: pseuCo.com
Area: process calculi, concurrent programming
Content: IDE for CCS & pseuCo (a concurrency-focused programming language with CCS-based semantics)
Usage: immediately usable in your browser – get started here: https://pseuco.com/#/sku/default/tool/landing

Other

• Name: DOMtutor