004 Datenverarbeitung; Informatik
Filtern
Erscheinungsjahr
Dokumenttyp
- Diplomarbeit (185)
- Bachelorarbeit (163)
- Studienarbeit (137)
- Ausgabe (Heft) zu einer Zeitschrift (126)
- Masterarbeit (84)
- Dissertation (48)
- Konferenzveröffentlichung (6)
- Buch (Monographie) (1)
- Habilitation (1)
- Bericht (1)
Sprache
- Deutsch (546)
- Englisch (203)
- Mehrsprachig (3)
Schlagworte
- Bildverarbeitung (13)
- Augmented Reality (10)
- Computersimulation (10)
- Robotik (10)
- Computergraphik (9)
- OpenGL (8)
- Routing (8)
- Semantic Web (8)
- Computerspiel (7)
- Informatik (7)
Institut
- 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)
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)
Die hohen Infrastrukturkosten machen das Überprüfen von Theorien bezüglich großer Rechnernetze zu einer schwierigen und teuren Aufgabe. Ein möglicher Ansatz dieses Problem zu beheben ist die Verwendung von virtueller anstelle von physikalischer Infrastrukur. OPNets IT Guru ist ein Programm, das entworfen wurde zur Simulation großer Netze und zur Repräsentation relevanter Informationen. Es gestattet großflächige Änderungen zu testen oder Theorien zu überpruefen ohne den Aufwand einer physikalischen Infrastruktur.
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.
Die vorliegende Diplomarbeit thematisiert die quantitative Analyse und die Visualisierung von Infarktgewebe des linken Herzmuskels. Im Mittelpunkt der Untersuchung steht das Ausmaß der Narbe und deren Deformation ueber den Herzzyklus. Fuer die Narbenausdehnung stehen so genannte Late-Enhancement-Daten zur Verfuegung, die das avitale Gewebe durch ein Kontrastmittel hervorheben. Anhand von automatisierten Verfahren wird die Narbe aus den Bilddaten extrahiert und auf ihre Groesse, Lokalisation und Transmuralitaet quantifiziert. Die Transmuralitaet gibt dabei das lokale Verhaeltnis zwischen der Herzwand- und der Narbenbreite an. Des Weiteren wird die Narbe für die Beurteilung der Beschaffenheit dreidimensional in dem Analysefenster dargestellt. Der Mediziner kann durch das entwickelte Verfahren innerhalb kuerzester Zeit Aussagen ueber das Ausmass und den Ursprung des Herzinfarktes treffen und zudem die Ergebnisse durch verschiedene visuelle Darstellungen kontrollieren. Die Deformation des Narbengewebes über den Herzzyklus und deren Integration mit den dynamischen Cine-Daten wurde bereits in einer vorangegangenen Diplomarbeit umgesetzt. Im Rahmen dieser Arbeit wird eine visuelle Verbesserung der Deformationsergebnisse angestrebt, die das Narbengewebe aus den Volumendaten extrahiert. Das avitale Gewebe wird durch das Eliminieren von uninteressanten Bildinformationen hervorgehoben und verbessert somit die visuelle Analyse der Narbendeformation ueber den Herzzyklus. Beide Verfahren liefern eine detaillierte und eindeutige Analyse des Infarktgewebes, die die manuelle Untersuchung in der klinischen Praxis ergaenzen kann.
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.
Partielle Wissenskompilation
(2006)
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.
Die vorliegende Arbeit bietet ein Konzept für die Implementierung eines Web-Usage-Mining-Systems. Besonderer Schwerpunkt der Arbeit ist die Orientierung an Anwendungsgebieten mit hohem Besuchsaufkommen. Dazu liefert die Arbeit einen Ueberblick ueber ausgewaehlte Messmethoden und Erfassungstechniken für die Nutzungsanalyse von Web-Zugriffen und bietet zu den einzelnen Aspekten Strategien an, die auch bei hohem Datenaufkommen pertinente Speicher- und Abfragekomplexitaet gewaehrleisten.
In den letzten Jahren konzentrierte sich das E-Government auf die administrativen Aspekte der Verwaltungsmodernisierung. Im nächsten Schritt werden die E-Diskurse als Instrument der Bürgernähe und Mittel der E-Demokratie/E-Partizipation an Bedeutung gewinnen. Mit zunehmender Akzeptanz solcher E-Diskurse werden diese schnell eine Komplexität erreichen, die von den Teilnehmern nicht mehr zu bewältigen ist. Das Problem liegt in der eingeschränkten Möglichkeit, einen in Raum und Zeit verteilten Diskurs zu verfolgen und sich ein Bild von ihm zu machen. Viele Eindrücke, die sich aus Präsenzdiskussionen gewinnen lassen, fehlen. Deswegen hat die vorliegende Arbeit die Zielsetzung der Konzeption und der prototypischen Implementierung eines Instrumentariums (Diskursmeter), womit sich die Teilnehmer, insbesondere die Moderatoren, des E-Diskurses jederzeit einen Überblick über den E-Diskurs schaffen können und so zu ihrem Diskursverständnis (Discourse Awareness) zu gelangen. Über das aktuelle Geschehen im E-Diskurs informiert die gegenwartsorientierte und über das vergangene Geschehen die vergangenheitsorientierte Discourse Awareness, über die etwaige Trends sichtbar sind. Der Fokus der Discourse Awareness liegt in der quantitativen Betrachtung des Geschehens im E-Diskurs. Aus dem in dieser Arbeit entwickelten Modell des E-Diskurses resultieren die Fragestellungen zur Discourse Awareness, deren Konkretisierung Grundlage für die Implementierung des Diskursmeters ist. Die an das Modell des E-Diskurses angebrachten Diskurssensoren zeichnen das Geschehen im E-Diskurs auf, die zu Diskursereignissen führen, die das Diskursmeter in unterschiedlichen Visualisierungsformen präsentiert. Den Moderatoren des E-Diskurses bietet das Diskursmeter die gegenwartsorientierte Discourse Awareness als Monitoring und die vergangenheitsorientierte Discourse Awareness als Abfrage (quantitative Analyse) an.
Der Einsatz von Computern hat in den vergangenen Jahrzehnten die Arbeitsweise von Sozialwissenschaftlern nachhaltig verändert. Es ist wohl nicht übertrieben zu behaupten, daß die Verbreitung und zunehmende Bedienungsfreundlichkeit von Rechenanlagen und statistischen Auswertungsprogrammen der empirischen Sozialforschung als vorherrschender Forschungsstrategie erst zum Durchbruch verholfen haben. Mit der steigenden Bedeutung von Computern im sozialwissenschaftlichen Forschungsprozeß ist auch eine neue Wissenschaftsdisziplin entstanden, die sich schwerpunktmaßig mit der Adaption und Anwendung von Werkzeugen und Methoden der Informatik in der sozialwissenschaftlichen Forschung beschäftigt: die Sozialwissenschaftliche Informatik. Das vorliegende Skript ist aus einer Reihe von Vorlesungen hervorgegangen, die wir für Studierende dieses Anwendungsfaches im Studiengang Diplom-Informatik an der Universität Koblenz-Landau gehalten haben. Im Gegensatz zu vielen anderen Einführungen in die uni- und multivariate Datenanalyse richtet sich die vorliegende Darstellung der statistischen Verfahren in erster Linie an fortgeschrittene Anwender der "klassischen" statistischen Methoden, die sich einen Überblick über die mathematischen Grundlagen der angewandten Methoden verschaffen und bei der Interpretation ihrer Analyseergebnisse die Fallstricke rezeptbuchartiger Einführungen vermeiden möchten. Dieses elektronische Dokument ist die geringfügig überarbeitete Fassung des 1994 erschienenen Buches, welches seit langem vergriffen ist.
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.