Informatikpraktikum 1 (185.253),
Informatikpraktikum 2 (185.955),
Freifachpraktikum (185.279),
Projektpraktikum für Informatik (185.285),
Project in Computational Logic (185.302).
Betreuer: Bernhard Gramlich
Wenn Sie sich für eines der angeführten Themen interessieren,
wenden Sie sich bitte direkt an mich (Email:
gramlich@logic.at, Tel.:
58801-18544, Sprechstunde siehe
hier bzw. nach Vereinbarung).
Die Themen können auch in kleinen Gruppen bearbeitet
werden.
Andere als die unten angegebenen Themen sind nach Absprache
ebenfalls möglich. Dazu zählen insbesondere solche Themen,
die in einem inhaltlichen Zusammenhang zu einer der Vorlesungen
Termersetzungssysteme
(siehe auch VMTL - Vienna Modular Termination Tool),
Computational Equational Logic,
Formale Methoden der Informatik und
Semantik von Programmiersprachen
stehen.
Angebotene Praktikumsthemen (u.a.):
Background: VMTL is a tool for the automated verification of termination of term rewriting systems. The task of proving termination involves the search for suitable interpretations of terms and/or orderings on terms. Basically, this search is a constraint satisfaction problem. One practically efficient way to solve such problems is by encoding them in a satisfiability (SAT) problem and utilize dedicated SAT solvers to obtain a solution. To this end a Java interface is to be developed that encapsulates the preparation and solving of boolean formulas through external SAT solvers.
Task:
Write a Java program that accepts a
boolean formula (as string or Java object) and
returns a model for the formula or "no" in case
the formula is unsatisfiable. For the actual
SAT solving task an external SAT solver is to
be used. Efficiency is a major concern.
Optional:
Use the library to (re-)implement
certain processors in VMTL.
Prerequisites: Propositional logic, Java.
For the optional part:
Foundational knowledge in theoretical computer
science/mathematics and term rewtiting (i.e., terms, trees, orderings, ...).
Supervisor(s): Bernhard Gramlich, Felix Schernhammer.
Home Page B.G. | LVAs B.G. | LVAs 185/2 | Home Page B.G. | AG 185/2 | Institut 185 | Server Home Page | Faculty of Informatics | TU Wien
Bernhard Gramlich