-
Specification and Automatic Verification of Computational Reductions
Authors:
Julien Grange,
Fabian Vehlken,
Nils Vortmeier,
Thomas Zeume
Abstract:
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 pro…
▽ More
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.
△ Less
Submitted 4 July, 2024;
originally announced July 2024.
-
Iltis: Learning Logic in the Web
Authors:
Gaetano Geck,
Christine Quenkert,
Marko Schmellenkamp,
Jonas Schmidt,
Felix Tschirbs,
Fabian Vehlken,
Thomas Zeume
Abstract:
The Iltis project provides an interactive, web-based system for teaching the foundations of formal methods. It is designed with the objective to allow for simple inclusion of new educational tasks; to pipeline such tasks into more complex exercises; and to allow simple inclusion and cascading of feedback mechanisms. Currently, exercises for many typical automated reasoning workflows for propositio…
▽ More
The Iltis project provides an interactive, web-based system for teaching the foundations of formal methods. It is designed with the objective to allow for simple inclusion of new educational tasks; to pipeline such tasks into more complex exercises; and to allow simple inclusion and cascading of feedback mechanisms. Currently, exercises for many typical automated reasoning workflows for propositional logic, modal logic, and some parts of 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 courses over the last years, many of them with more than 300 students.
We invite all readers to try out Iltis: https://iltis.cs.tu-dortmund.de
△ Less
Submitted 27 May, 2022; v1 submitted 12 May, 2021;
originally announced May 2021.
-
Introduction to Iltis: An Interactive, Web-Based System for Teaching Logic
Authors:
Gaetano Geck,
Artur Ljulin,
Sebastian Peter,
Jonas Schmidt,
Fabian Vehlken,
Thomas Zeume
Abstract:
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. The Iltis project aims at providing a web-based, interactive system that sup…
▽ More
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. The Iltis project aims at providing a web-based, interactive system that supports teaching logical methods. In particular the system shall (a) support to learn to model knowledge and to infer new knowledge using propositional logic, modal logic and first-order logic, and (b) provide immediate feedback and support to students. This article presents a prototypical system that currently supports the above tasks for propositional logic. First impressions on its use in a second year logic course for computer science students are reported.
△ Less
Submitted 4 April, 2018;
originally announced April 2018.
