The project consists of finding appropriate tools which can help in learning concepts presented in the Term Rewriting lecture and installing them (under supervision). The main systems designed for the problems in term rewriting can be found at http://rewriting.loria.fr.
A student will have to choose appropriate systems, get to know their functionality and design a common interface. The main problems which should be possible to solve with the help of the existing tools are:
Since different systems may have different input/output formats, the decision should be made on one such format, which is then translated depending on which system is going to be used to solve a specific problem. A short manual should be written describing how to use the tools for term rewriting, i.e. how to write correct input, how to trigger a desirable action and what is the form of the output.Literature:
Molecular Computing, known also under the name Biological Computing (computing in test tubes), is a new computation paradigm that employs DNA molecule manipulation to solve mathematical problems. Some aspects such as the high data density allow one to achieve parallel reactions in a test tube. Many computationally complete models of biological computers are developed and many experiments are executed e.g. DNA Haskell. As a special programming language DNA Haskell supports the construction of DNA algorithms which should be executed in labs via molecular biological techniques. Experimental studies on Molecular Computing are prepared on the basis of these algorithms.
Objective of the Komplexpraktikum are:
Two-way Alternating automata (2ATAs) on infinite trees are an elegant approach to deciding satisfiability in a broad range of logics. For many such applications in logic, it is important that the emptiness problem of 2ATAs can be checked in deterministic exponential time. Unfortunately, this result is scattered across several papers, and a clear and straight- forward presentation is missing. The goal of this project is to locate and read the relevant literature, and to produce a direct and self-contained proof of the fact that the emptiness problem for 2ATAs is in ExpTime.
Note that this is a theoretical project: it does not involve implementation, but requires the participants to prove some theoretical results.Literature: will be provided.