004 Datenverarbeitung; Informatik
Refine
Year of publication
Document Type
- Diploma Thesis (185)
- Bachelor Thesis (163)
- Study Thesis (137)
- Part of Periodical (126)
- Master's Thesis (84)
- Doctoral Thesis (48)
- Conference Proceedings (6)
- Book (1)
- Habilitation (1)
- Report (1)
Language
- German (546)
- English (203)
- Multiple languages (3)
Keywords
- Bildverarbeitung (13)
- Augmented Reality (10)
- Computersimulation (10)
- Robotik (10)
- Computergraphik (9)
- OpenGL (8)
- Routing (8)
- Semantic Web (8)
- Computerspiel (7)
- Informatik (7)
Institute
- Fachbereich 4 (273)
- Institut für Computervisualistik (222)
- Institut für Informatik (114)
- Institut für Wirtschafts- und Verwaltungsinformatik (104)
- Institut für Management (49)
- Institut für Softwaretechnik (47)
- Institute for Web Science and Technologies (34)
- Institut für Integrierte Naturwissenschaften (4)
- An-Institute (1)
Problems in the analysis of requirements often lead to failures when developing software systems. This problem is nowadays being faced by requirements engineering. The early involvement of all kinds of stakeholders in the development of such a system and a structured process to elicitate and analyse requirements have made it a crucial factor as a first step in software development. The increasing complexity of modern softwaresystems though leads to a rising amount of information which has to be dealt with during analysis. Without the support of appropriate tools this would be almost impossible to do. Especially in bigger projects, which tend to be spatially distributed, an effective requirements engineering could not be implemented without this kind of support. Today there is a wide range of tools dealing with this matter. They have been in use since some time now and, in their most recent versions, realize the most important aspects of requirements engineering. Within the scope of this thesis some of these tools will be analysed, focussing on both the major functionalities concerning the management of requirements and the repository of these tools. The results of this analyis will be integrated into a reference model.
Erweiterung der Spielegraphik von Cam2Dance durch den Einsatz von Shadern und komplexen Modellen
(2006)
Prävention von Korruption
(2006)
The known methods of the prevention of corruption are set into context of comparable ways to obviate accidences during working processes, environmental pollution by organisations and the options to ensure quality for manufactured goods. The aim was to find out if and in which degree the different methods of prevention in the area of corruption and the mentioned aspects of the TQM support each other.
Shadows add a level of realism to a rendered image. Furthermore, they support the user of an augmented reality application through the interactions of virtual objects. The reason for this is that shadows make it easier to judge the position and the size of a virtual object. In 1978, Lance Williams published the shadow mapping algorithm with the aim to render a shadow of objects in a virtual scene. This master thesis presents a modified shadow mapping approach that can additionally be used in Augmented/Mixed Reality applications. First of all the standard algorithm ist extended by a PCF-filter. This filter is used to handle the aliasing-problem on the edges of the shadow and also to soften the shadow. Phantom objects are necessary to be able to operate this approach in a Mixed Reality application. These objects simulate the position and the geometry of the real objects for the algorithm. The approach consists of three steps: First the camera image is drawn into the framebuffer. After that a shadow map, of the virtual objects only, is created. When rendering these objects shadow mapping creates the shadows of virtual objects onto other virtual objects and on themselves. Afterwards the phantom objects are rendered. The depth test is performed on the fragment shader. If a fragment lies in a shadowed region it will get the color of the shadow. However, if it is beeing lit its transpareny value will be set to 1 so that it will not be seen. By applying this procedure all shadows from the virtual objects onto the real objects will be drawn. The results show that the approach can be used in real time in Mixed Reality environments. Additionally a comparison with a modified version of a shadow volume algorithm that can also be used for Mixed Reality applications shows that the approach of this master thesis casts a more realistic shadow in a shorter period of time. All in all this approach increases the level of realism in augmented reality applications and it helps the user measure distances and sizes of the virtual objects more easily.
Emotion Video
(2006)
Gefühle durch ein Medium übertragen, das klingt unglaublich und doch hat es einen grossen Reiz. Was könnten wir alles machen? Wir könnten dabei sein, wenn ein Astronaut in den Weltraum fliegt oder einen Sonnenaufgang in der Südsee erleben ohne dort zu sein. Man könnte die Gefühle eines Gewinners ebenso weitergeben, wie die einer Person, die Angst hat. Aber auch andere Aspekte, wie die Arbeit aus Sicht eines Profis zu betrachten oder etwas Neues kennenzulernen wäre möglich. Den eigenen Tag, die letzte Woche oder sogar weit zurückliegende Ereignisse aus dem eigenen Leben noch einmal erleben, das alles macht den Anreiz an diesem Thema aus. Der Aufbau dieser Arbeit soll die Entwicklung von der Entstehung von Emotionen beim Menschen über die technischen Möglichkeiten zur Aufzeichnung von Sinneswahrnehmungen bis zum Gesamtkonzept mit prototypischer Umsetzung zeigen. Zunächst soll geklärt werden, was nötig ist um Emotionen "einzufangen" und zu konservieren und welche Möglichkeiten sich für die Wiedergabe dieser anbieten. Zentral soll ein Konzept sein, welches die momentanen technischen Möglichkeiten berücksichtigt, aber auch darüber hinaus aufzeigt, was wichtig und nötig wäre um dem Ziel möglichst nahe zu kommen, Emotionen zu übertragen. Dieses Konzept soll im Anschluss prototypisch umgesetzt werden um es so zu evaluieren. Dabei soll eine erweiterbare Plattform zunächst zur Aufzeichnung visueller und auditiver Reize entwickelt werden.
Zielsetzung: Für die Feuerwehr- und Katastrophenschutzschule Rheinland - Pfalz (LFKS) sollen auf der Basis von Flash und XML interaktive Quizzes realisiert werden, die im Rahmen des Gruppenführerlehrgangs als Lernerfolgskontrolle dienen sollen. Als Grundlage wird ein selbstentwickeltes MVC Framework und Adobe (ehemals Macromedia) Flash herangezogen.
Entwicklung: Bei der Entwicklung der Quizzes wurde sehr viel Wert auf eine systemunabhängige, bestmöglich standardisierte Datenhaltung gelegt. Hier war die Verbindung von Flash und XML eine optimale Lösung.
Technik: Mit der Kombination aus ActionScript2, XML und Flash ist es möglich, innerhalb kürzester Zeit unterschiedliche Quizzes zu erstellen. Der Grundgedanke bei dieser Technik ist es, Daten und ihre Repräsentation zu trennen. Die Flash Entwicklungsumgebung wird für die Erstellung der Views (Darstellungselemente) verwendet. Die Views werden anhand von dynamischen Textfeldern, interaktiven Animationen und weiteren Darstellungselementen definiert. Diese Views werden über das MVC-Framework mit Actionscript2 angesprochen und mit Inhalten aus einer externen XML Datei gefüllt. Der Vorteil dabei ist, dass die Inhalte und zum Teil auch das Design recht schnell ausgewechselt werden können, ohne an der Applikation Änderungen vornehmen zu müssen. Die XML Dateien werden mit Hilfe der Software Infopath der Firma Microsoft erstellt. Eine weitere Möglichkeit die Daten zu standardisieren ist das IMS Question and Test Interoperability (IMS QTI) Datenformat, welches explizit für solche Anwendungen entwickelt wurde. Dieses Format wird jedoch nur am Rande behandelt. Diese Flashapplikationen können sowohl als eigenständige Programme betrachtet oder als Elemente einer HTML Datei in einem Browser dargestellt werden. Aus diesem Grund ist es möglich, auf fast jedem Gerät (PC, Notebook, Handheld und Mobiltelefon) und auf jedem Betriebssystem (Windows, Mac OS, Linux, etc.) eine Flashapplikation zum Laufen zu bringen.
Ausblick: Durch das selbstentwickelte MVC-Framework kann die Applikation schnell und einfach erweitert werden. Es wurde jedoch drauf geachtet, dass die Applikation auch ohne den Quellcode neu zu kompilieren vom Aussehen verändert werden kann.
Szeneneditor für ein Echtzeitanimationssystem und andere XML konfigurierte und erweiterbare Systeme
(2006)
The high cost of routing infrastructure makes checking theories about larger nets a very difficult and expensive task. One possible approach to fight this problem is the use of virtual instead of physical infrastructure. OPNet- IT Guru software is a suite designed to simulate large nets and present relevant information. This allows validating extensive changes before actually implementing them on a productive network or testing theories without the overhead of a physical infrastructure.
In dieser Studienarbeit wird ein Verfahren zur Extraktion eines Oberflächenbegrenzungsmodells aus einem Tiefenbild vorgestellt. Das Modell beschreibt die im Tiefenbild dargestellte Szene durch die Geometrie und die Topologie der planaren Flächen, die in der Szene gefunden werden. Die Geometrie ist gegeben durch die Angabe der Ebenengleichungen der gefundenen Flächen sowie der 3D-Koordinaten der Eckpunkte der Polygone, die diese Flächen beschreiben. Die Informationen über die Topologie der Szene besteht aus einer Nachbarschaftsliste, die für jede Flaeche angibt, über welche Kante diese Fläche mit welcher anderen Fläche verbunden ist. Aufbauend auf einem Algorithmus zur Tiefenbildsegmentierung aus PUMA werden die Polygone bestimmt, die die Flächen der Szene beschreiben. Anschließend wird versucht, diese Polygone über Kanten und Eckpunkte zu verbinden, um ein möglichst geschlossenes Modell der Szene zu erhalten.
XDOMEA-Fachkonzept
(2006)
Die AG "IT-gestützte Vorgangsbearbeitung" des Kooperationsausschusses Automatisierte Datenverarbeitung (koopA ADV) hat zur Verwirklichung der Interoperabilität in der öffentlichen Verwaltung den Datenaustauschstandard XDOMEA entwickelt. Das vorliegende Dokument beschreibt das Fachkonzept zur XML-Schema-Spezifikation. Es wendet sich vorrangig an verantwortliche Organisatoren im IT-Bereich und an potentielle Anwender von XDOMEA. In diesem Dokument werden Hintergründe, Einsatzmöglichkeiten und Informationen zum Einsatzgebiet von XDOMEA erläutert, die Vorteile des Standards diskutiert und Erweiterungsmöglichkeiten vorgestellt. Weiters werden Beteiligungs- und Protokollinformationen spezifiziert und detailliert. Zu diesem Zweck werden verschiedene Szenarien erarbeitet, die anhand von Prozessmodellen die praktische Anwendung des Standards veranschaulichen. Gleichzeitig werden die Möglichkeiten fachspezifischer Erweiterungen im Standard verdeutlicht und Grenzen der Anwendung aufgezeigt.
Die Zeitschrift c't stellte in der Ausgabe 02/2006 einen Bausatz für einen kleinen mobilen Roboter vor, den c't-Bot, der diese Studienarbeit inspirierte. Dieser Bausatz sollte die Basis eines Roboters darstellen, der durch eine Kamera erweitert und mit Hilfe von Bildverarbeitung in der Lage sein sollte, am RoboCupSoccer-Wettbewerb teilzunehmen. Während der Planungsphase veränderten sich die Ziele: Statt einem Fußballroboter sollte nun ein Roboter für die neu geschaffene RoboCup-Rescue-League entwickelt werden. In diesem Wettbewerb sollen Roboter in einer für sie unbekannten Umgebung selbstständig Wege erkunden, bzw. Personen in dieser Umgebung finden. Durch diese neue Aufgabenstellung war sofort klar, dass der c't-Bot nicht ausreichte, und es musste ein neuer Roboter entwickelt werden, der mittels Sensoren die Umgebung wahrnehmen, durch eine Kamera Objekte erkennen und mit Hilfe eines integrierten Computers diese Bilder verarbeiten sollte. Die Entstehung dieses Roboters ist das Thema dieser Studienarbeit.
iProcess
(2006)
Das performante Rendering großer Volumendaten stellt trotz stetig gestiegener Prozessorleistungen nach wie vor hohe Anforderungen an jedes zugrunde liegende Visualisierungssystem. Insbesondere trifft dies auf direkte Rendering-Methoden mithilfe des Raycasting-Verfahrens zu, welches zum einen eine sehr hohe Qualität und Genauigkeit der generierten Bilder bietet, zum anderen aber aufgrund der dafür nötigen hohen Abtastrate relativ langsam ist. In dieser Studienarbeit wird ein Verfahren zur Beschleunigung des Raycasting- Visualierungsansatzes vorgestellt, das auf adaptivem Sampling beruht. Dabei werden statische Volumendaten zunächst in einem Vorverarbeitungsschritt einer Gradientenanalyse unterzogen, um so ein Interessensvolumen zu erstellen, das wichtige und weniger wichtige Bereiche kennzeichnet. Dieses Volumen wird anschließend von einem Raycaster genutzt, um adaptiv für jeden Abtaststrahl die Schrittweite zu bestimmen.
Currently more than 850 biological databases exist. The majority of biological knowledge is not in these databases but rather contained as free text in scientific literature. For systems biology tasks it is often necessary to integrate and extract data from heterogeneous databases and free text as well as to analyse the information in the context of experimental data. ONDEX is an integration framework which aims to address these challenges by combining features of database integration, text mining and sequence analysis with methods for graph-based data analysis and visualisation. The main topics of this diploma thesis are the redesign of the ONDEX backend, the development of a data exchange format, the development of a query environment and the allocation of Web services for data integration, data exchange and queries. These Web services allow backend workflow control from both local and remote workstations.
Die Leistungsfähigkeit moderner Graphikkarten steigt zur Zeit schneller an, als die von CPUs. Dabei kann diese Leistung nicht nur zur Darstellung von 3D Welten, sondern auch für allgemeine Berechnungen (GPGPU) verwendet werden. Diese Diplomarbeit untersucht daher, ob mit Hilfe der GPU Volumendaten schneller gefiltert werden können, als mit der CPU. Dies soll insbesondere am Beispiel von Rausch-Filtern, die auf Videosequenzen angewendet werden, untersucht werden. Dabei soll das Video als Volumen repräsentiert und mit Volumenfiltern gefiltert werden. So soll eine höhere Qualität und eine kürzere Berechnungszeit als mit herkömmlichen CPU und Frame-basierten Verfahren erreicht werden, insbesondere auch bei den z.Z. stark aufkommenden hochauflösenden HDTV-Standards. Das Framework soll jedoch nicht auf Videosequenz-Bearbeitung beschränkt sein, sondern so konzipiert werden, dass es z.B. in bestehende Volumenvisualisierungssysteme integriert werden kann. Das Ziel der Arbeit ist die Einarbeitung in die notwendigen theoretischen Grundlagen, daran anschließend die prototypische Implementierung des Frameworks mit abschließender Bewertung der erreichten Ergebnisse insbesondere der Geschwindigkeit im Vergleich zu existierenden Systemen.
Die moderne Bildgebung in der Medizin arbeitet oft mit Daten höheren Tonwertumfangs. So haben beispielsweise Bilder aus CT-Geräten einen Dynamikbereich von 12 Bit, was 4096 Graustufen entspricht. Im Bereich der photorealistischen Computergrafik und zunehmend in der Bildverarbeitung sind Bilddaten viel höheren Tonwertumfangs üblich, die als HDR-Bilder (High Dynamic Range) bezeichnet werden. Diese haben eine Bittiefe von 16, oftmals sogar 32 Bit und können dadurch sehr viel mehr Informationen speichern, als herkömmliche 8-Bit-Bilder. Um diese Bilder auf üblichen Monitoren darstellen zu können, muss man die Bildinformation auf den Tonwertumfang des Ausgabegerätes abbilden, was man als Tonemapping bezeichnet. Es existieren zahlreiche solcher Tonemapping-Verfahren, die sich durch ihre Arbeitsweise, Geschwindigkeit und visuelle Qualität unterscheiden lassen. Im Rahmen dieser Studienarbeit sollen Tonemapping-Verfahren auf medizinische Bilddaten angewendet werden. Dabei soll sowohl die visuelle Qualität, als auch die Geschwindigkeit im Vordergrund stehen.
Die Planung in Form eines visuellen Entwurfs ist schon seit jeher Bestandteil des Prozesses der Entwicklung von Artefakten aller Art. Heutzutage wird der visuelle Entwurf zukuenftiger Produkte mithilfe von CAD-Systemen umgesetzt. Im ersten Teil der Arbeit wird daher ein einfaches System implementiert und erlaeutert, das die grundlegenden Funktionen umsetzt, die auch in professionellen CAD-Systemen unerlaesslich sind. Im zweiten Teil werden ueber die Grundfunktionen hinaus ausgewaehlte Algorithmen der parametrischen Modellierung vorgestellt, die die Grundlage fuer die leistungsfaehigen, flexiblen und produktiven Systeme im modernen computer-unterstuetzten Entwurf bilden.
Program slicing is a technique for extracting that parts of a program which influence a previously defined, so-called slicing criterion. The latter mostly takes the form of a source code statement and a set of variables. Over the years an abundance of variants and enhancements has evolved from the original notion of a program slice. One of these developments is called chopping. A chop only contains those statements which are necessary to sustain the effects of a certain statement on another statement. Corresponding to the slicing criterion, the two statements have to be available in advance. This diploma thesis deals with the development of a service model in order to support the computation of a slice or a chop, given an original program and a slicing or chopping criterion respectively. A service model is a framework of communicating services so that each service performs a specific task within the concept of program slicing. The three main tasks, without considering further decomposition, are the mapping of program code into a representation suitable for slicing, the slicing itself and the display of the slice as code. The key benefit of service-orientation is that a service encapsulates the underlying algorithms. Hence the possibility of improving or substituting them without changing the interfaces of the related service relieves the developer of the need of adapting adjoining services. Thus, service-orientation fosters maintainability and improvability. Besides the definition of the services, this thesis also partially formally defines the data flow between them, i.e. their interfaces. It also features graph class definitions for most data structures. An accurate description of the interfaces encourages reuse, provided the services are of adequate granularity.
Interactive video retrieval
(2006)
The goal of this thesis is to develop a video retrieval system that supports relevance feedback. One research approach of the thesis is to find out if a combination of implicit and explicit relevance feedback returns better retrieval results than a system using explicit feedback only. Another approach is to identify a model to weight existing feature categories. For this purpose, a state-of-the-art analysis is presented and two systems implemented, which run under the conditions of the international TRECVID workshop. It will be a basis system for further research approaches in the field of interactive video retrieval. Amongst others, it shall participate in the 2006 search task of the mentioned workshop.
This work represents a quantitative analysis and visualisation of scar tissue of the left ventricular myocard. The scar information is shown in the late enhancement data, that highlights the avitale tissue with the help of a contrast agent. Through automatic methods, the scar is extracted from the image data and quantifies the size, location and transmurality. The transmurality shows a local measurement between the heart wall und the width of the scar. The developed methods help the cardiologist to analyse the measurement, the reason and the degree of the heart failure in a short time period. He can further control the results by several visual presentations. The deformation of the scar tissue over the heart cycle is implemented in another scientific work. A visual improvement of the deformation result which extracts the scar out of the data is aspired. The avital tissue is shown in a more comfortable way by eliminating the unnecessary image information and therefore improves the visual analysis of the pumping heart. Both methods show a detailed analysis of the scar tissue. This supports the clinic practical throughout the manual analysis.
Ein Interpreter für GReQL 2
(2006)
Im Rahmen dieser Diplomarbeit wird die Auswertungskomponente fuer die Graphanfragesprache GREQL 2, welche von Katrin Marchewka beschrieben wurde, entworfen, welche Anfragen diese Sprache interpretiert. Die Auswertungskomponente besteht aus den Bausteinen Auswerter, Parser, Optimierer, Funktionsbibliothek und dem Containerframework JValue. Der Parser wurde bereits von Katrin Marchewka implementiert, der Optimierer bleibt einer Anschlußarbeit vorbehalten. Innerhalb dieser Arbeit werden die Bausteine Auswerter, Funktionsbibliothek und JValue als Prototypen implementiert. Aufgrund der Erfahrungen mit der Auswertungskomponente fuer den GREQL 2-Vorgaenger GREQL 1 ist das Primaerziel dieser Arbeit der Entwurf einer sauberen, klaren, erweiterbaren und zukunftsfähigen Architektur, wobei die aktuellen Prinzipien der Softwaretechnik beüecksichtigt werden sollen.
Viele Probleme in der Aussagenlogik sind nur sehr aufwändig lösbar. Ist beispielsweise eine Wissensbasis gegeben, an die wir Anfragen stellen, wollen, so kann dies mitunter sehr mühsam sein. Um trotzdem effizient Anfragen beantworten zu können, hat sich die Vorgehensweise der Wissenskompilation entwickelt. Dabei wird die Lösung der Aufgabe in eine Offline- und eine Online-Phase aufgeteilt. In der Offline-Phase wird die Wissensbasis präkompiliert. Dabei wird sie in eine bestimmte Form umgewandelt, auf der sich die erwarteten Anfragen effizient beantworten lassen. Diese Transformation der Wissensbasis ist meist sehr aufwändig, muss jedoch nur einmalig durchgeführt werden. In der darauffolgenden Online-Phase können nun effizient Anfragen beantwortet werden. In dieser Diplomarbeit wird eine spezielle Normalform, die sich als Zielsprache der Präkompilation anbietet, untersucht. Außerdem wird die Präkompilation so in einzelne Schritte unterteilt, dass möglicherweise bereits nach einigen Teilschritten Anfragen beantwortet werden können.
This document presents a concept of a "web usage mining system". The main purpose of this work is to cover situations, in which high traffic will cause traditional approaches to collapse. Therefore, it presents several measuring methods and acquisition techniques, and provides strategies that allow pertinent storage and querying complexity even in high traffic domains.
In the last years the e-government concentrated on the administrative aspects of administrative modernisation. In the next step the e-discourses will gain in importance as an instrument of the public-friendliness and means of the e-democracy/e-participation. With growing acceptance of such e-discourses, these will fastly reach a complexity, which could not be mastered no more by the participants. Many impressions, which could be won from presence discussions, will be lacking now. Therefore the exposed thesis has the objective of the conception and the prototypical implementation of an instrument (discourse meter), by which the participants, in particular the moderators of the e-discourse, are capable to overlook the e-discourse at any time and by means of it, attain their discourse awareness. Discourse awareness of the present informs about the current action in the e-discourse and discourse awareness of the past about the past action, by which any trends become visible. The focus of the discourse awareness is located in the quantitative view of the action in the e-discourse. From the model of e-discourse, which is developed in this thesis, the questions of discourse awareness are resulting, whose concretion is the basis for the implementation of the discourse meter. The discourse sensors attached to the model of the e-discourse are recording the actions of the e-discourse, showing events of discourse, which are represented by the discourse meter in various forms of visualizations. The concept of discourse meter offers the possibility of discourse awareness relating to the present as monitoring and the discourse awareness relating to the past as query (quantitative analysis) to the moderators of the e-discourse.
Computers fundamentally changed the methods used by social scientists during the past decades. It is no exaggeration to state that the wide use and growing user-friendliness of computers and statistical analysis systems helped empirical social research as a subdiscipline to become mainstream. This made a new subdiscipline necessary which is mainly working on adapting and applying computer science methods for social research: social science informatics. This book originated from lecture courses given by the authors from the mid-1980s and developed for computer science students with a minor in social science. Unlike many other introductions to univariate and multivariate data analysis, this book is addressed to advanced scholars and students who apply "classical" statistical methods and who want to get an overview of the mathematical foundations of the methods they apply and who want to avoid the pitfalls of cookbook-like introduction when they interpret their results. The electronic document is a slightly revised version of the printed version of 1994 which has been out of stock for many years.
We aim to demonstrate that automated deduction techniques, in particular those following the model computation paradigm, are very well suited for database schema/query reasoning. Specifically, we present an approach to compute completed paths for database or XPath queries. The database schema and a query are transformed to disjunctive logic programs with default negation, using a description logic as an intermediate language. Our underlying deduction system, KRHyper, then detects if a query is satisfiable or not. In case of a satisfiable query, all completed paths -- those that fulfill all given constraints -- are returned as part of the computed models. The purpose of our approach is to dramatically reduce the workload on the query processor. Without the path completion, a usual XML query processor would search the database for solutions to the query. In the paper we describe the transformation in detail and explain how to extract the solution to the original task from the computed models. We understand this paper as a first step, that covers a basic schema/query reaÂsoning task by model-based deduction. Due to the underlying expressive logic formalism we expect our approach to easily adapt to more sophisticated problem settings, like type hierarchies as they evolve within the XML world.
The model evolution calculus
(2004)
The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.
The Living Book is a system for the management of personalized and scenario specific teaching material. The main goal of the system is to support the active, explorative and selfdetermined learning in lectures, tutorials and self study. The Living Book includes a course on 'logic for computer scientists' with a uniform access to various tools like theorem provers and an interactive tableau editor. It is routinely used within teaching undergraduate courses at our university. This paper describes the Living Book and the use of theorem proving technology as a core component in the knowledge management system (KMS) of the Living Book. The KMS provides a scenario management component where teachers may describe those parts of given documents that are relevant in order to achieve a certain learning goal. The task of the KMS is to assemble new documents from a database of elementary units called 'slices' (definitions, theorems, and so on) in a scenario-based way (like 'I want to prepare for an exam and need to learn about resolution'). The computation of such assemblies is carried out by a model-generating theorem prover for first-order logic with a default negation principle. Its input consists of meta data that describe the dependencies between different slices, and logic-programming style rules that describe the scenario-specific composition of slices. Additionally, a user model is taken into account that contains information about topics and slices that are known or unknown to a student. A model computed by the system for such input then directly specifies the document to be assembled. This paper introduces the elearning context we are faced with, motivates our choice of logic and presents the newly developed calculus used in the KMS.