The topics of this
Komplexprakticum will be in the following areas:
Initial
meetingPeople who want to participate in the praktikum/project, but have serious reasons to not attend the initial meeting, please send an email until April 7th.
Position in curriculum- Course of studies Computation Logic; project (12 credits)
PrerequisitesOrganisation
- Each student is assigned a tutor, depending on the topic chosen. During the semester, there will be regular meetings of the student and his tutor.
- The results of the praktikum/project will be presented at the end of the semester in a talk given by the student.
Language
Participants DutiesIt is also the duty of the participants to reserve enough time for performing the project. The sharp deadline for finishing the project is the beginning of the following semester, i.e. the allowed time for the project is one semester plus the following semester break. Failure to finish the project in time will result in no credits to be given. It is the obligation of the participant to start the project in time, and to make appointments with the supervisor for regular meetings during the semester.
Topics
-
(1) Implementation of Tools for the Term Rewriting lecture. -
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:
- with a TRS and a term as an input, output a normal form of the term or a set of its normal forms;
- with a TRS as an input, decide its termination using the orders known from the lecture (lpo, polynomial order);
- with an equational theory as an input, perform its completion.
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:- Database of Rewriting Systems, http://rewriting.loria.fr/
- Franz Baader, Tobias Nipkow. Term Rewriting and All That, Cambridge University Press, 1998.
Prerequisites: Lecture "Term Rewriting Systems"
Tutor: Dr. Barbara Morawska,
- (2) Molecular Computing
-
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:
- Execution and checking all examples described in the book "Rechnen mit DNA - Eine Einführung in Theorie und Praxis", chapter 3 - main chapter about molecular biological operations. (Book is written in German.)
- Implementation of special sequences consisting of different kinds of molecular biological operations.
- Reparation of DNA strands after each operation execution in the sense of a compact description in the data structure.
- Th. Hinze, M. Sturm. "Rechnen mit DNA - Eine Einführung in Theorie und Praxis". Oldenbourg Wissenschaftsverlag München, 2004.
Prerequisites: Some knowledge of functional programming (Haskell, Hugs) and some understanding of concepts in biology and genetics would be helpful.
Tutor: Dr.-Ing. Monika Sturm,
- (3) The emptiness problem for alternating automata
-
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.
Prerequisites: The lecture "Automata and Logic".
Tutor: Dr. Carsten Lutz,
Barbara Morawska