004 Datenverarbeitung; Informatik
Filtern
Erscheinungsjahr
Dokumenttyp
- Ausgabe (Heft) zu einer Zeitschrift (73)
- Dissertation (33)
- Masterarbeit (29)
- Diplomarbeit (27)
- Bachelorarbeit (25)
- Studienarbeit (11)
- Konferenzveröffentlichung (4)
- Habilitation (1)
Sprache
- Englisch (203) (entfernen)
Schlagworte
- Software Engineering (6)
- Bluetooth (4)
- ontology (4)
- API (3)
- E-KRHyper (3)
- Enterprise 2.0 (3)
- Knowledge Compilation (3)
- OWL (3)
- OWL <Informatik> (3)
- Ontologie <Wissensverarbeitung> (3)
- Ontology (3)
- Semantic Web (3)
- UML (3)
- University (3)
- classification (3)
- computer clusters (3)
- model-based (3)
- Abduktion <Logik> (2)
- Akzeptanz (2)
- Annotation (2)
- Beschaffung (2)
- Bildverarbeitung (2)
- Campus Information System (2)
- Cloud Computing (2)
- Computer Graphics (2)
- Computergraphik (2)
- Computersimulation (2)
- Data Mining (2)
- Equality (2)
- Formale Ontologie (2)
- Graphik (2)
- Line Space (2)
- Linked Open Data (2)
- Logistik (2)
- Maschinelles Lernen (2)
- Modellgetriebene Entwicklung (2)
- Netzwerk (2)
- Neuronales Netz (2)
- OpenGL (2)
- Petri Nets (2)
- Petri-Netze (2)
- Propagation (2)
- RDF (2)
- Schlussfolgern (2)
- Serviceorientierte Architektur (2)
- Softwaretest (2)
- Theorem Proving (2)
- Usability (2)
- Volumen-Rendering (2)
- Wikipedia (2)
- XML (2)
- artificial neural networks (2)
- constraint logic programming (2)
- governance (2)
- hybrid automata (2)
- mobile phone (2)
- multi-agent systems (2)
- multimedia metadata (2)
- parallel algorithms (2)
- probability propagation nets (2)
- semantics (2)
- social media (2)
- social simulation (2)
- 101companies (1)
- 2019 European Parliament Election (1)
- 8C model (1)
- ABox (1)
- API Analysis (1)
- API Migratiom (1)
- API analysis (1)
- API-Analyse (1)
- AUTOSAR (1)
- Acceleration Structures (1)
- Action Recognition (1)
- Action Segmentation (1)
- Adaptation (1)
- Adaptive Services Grid (ASG) (1)
- Adobe Flex (1)
- Agenten (1)
- Agentenorientiertes Software Engineering (1)
- Agents (1)
- Algolib (1)
- Algorithm Engineering (1)
- Amazon Mechanical Turks (1)
- Analysis of social platform (1)
- Android <Systemplattform> (1)
- Anpassung (1)
- Architektur <Informatik> (1)
- Archivierung (1)
- Articles for Deletion (1)
- Association Rules (1)
- Auditing (1)
- Augenbewegung (1)
- Augmented Reality (1)
- Auslese (1)
- Auswahl (1)
- Automated Theorem Proving (1)
- Automated Theorem Proving Systems (1)
- Automatische Klassifikation (1)
- Automatisches Beweisverfahren (1)
- Automotive Systems (1)
- Avatar (1)
- B2B Integration (1)
- BPM (1)
- BPMN (1)
- BPMS (1)
- Bayes Procedures (1)
- Bayes-Netz (1)
- Bayesian Networks (1)
- Bebauungsdichte (1)
- Bedarfsanalyse (1)
- Bedarfsforschung (1)
- Befahrbarkeit (1)
- Beschreibungslogik (1)
- Bildanalyse (1)
- Bildsegmentierung (1)
- Biometric Authentication (1)
- Bipartiter Graph (1)
- Blickbewegung (1)
- Blickpunktabhängig (1)
- Blog marketing (1)
- Border Gateway Protocol (1)
- Border Gateway Protocol 4 (1)
- Business Collaboration (1)
- Business Process Modeling (1)
- Bürgerbeiteiligung (1)
- C++ (1)
- CSCW (1)
- Calculus (1)
- Casual Games (1)
- CodeBlue (1)
- Cold Chain (1)
- Coloskopie (1)
- Communication Networks (1)
- Computational biology (1)
- Compute Shader (1)
- Computer Security (1)
- Computer Vision (1)
- Computer assisted communication (1)
- Computeranimation (1)
- Computersicherheit (1)
- Computerspiel (1)
- Computertomografie (1)
- Computervisualistik (1)
- Conference (1)
- Container Entity Modell (1)
- Content Analysis (1)
- Content Management (1)
- Context-aware processes (1)
- Core Ontology on Multimedia (1)
- Core Ontology on Multimedia (COMM) (1)
- Creativity (1)
- Criteria Matrix (1)
- Crowdsourcing (1)
- DPLL procedure (1)
- DTI (1)
- Darmpolyp (1)
- Data compression (1)
- Data manipulation (1)
- Data protection (1)
- Datenaustausch (1)
- Datenkompression (1)
- Datenschutz (1)
- Deduktion (1)
- Deep Metric Learning (1)
- Defi-Now! (1)
- Defibrillator (1)
- Delta (1)
- Description Logic (1)
- Description Logics (1)
- Design Pattern (1)
- Destiny (1)
- Developer profiling (1)
- Diabetes (1)
- Diabetische Retinopathie (1)
- Diagnose (1)
- Diagnoseunterstützung (1)
- Diagnosis (1)
- Diagnosis assistance (1)
- Diffusion (1)
- Diffusionsbildgebung (1)
- Digitale Bilder (1)
- Dijkstras Algorithmus (1)
- Dimension 3 (1)
- Dimensionality Reduction (1)
- Dimensionsreduzierung (1)
- Discussion Forums (1)
- Diskrete Simulation (1)
- Distance Vector Routing (1)
- Distanz Vektor Routing (1)
- Distributed Environments (1)
- Distributed process execution (1)
- Dokumentation (1)
- Drahtloses lokales Netz (1)
- Dreidimensionale Bildverarbeitung (1)
- Driver Assistance Systems (1)
- Dynamische Analyse (1)
- E-Business (1)
- E-Hyper Tableau (1)
- E-KRHyper theorem prover (1)
- E-Partizipation (1)
- E-government (1)
- E-participation (1)
- E-services (1)
- ECMS 2012 (1)
- EU (1)
- Eclipse <Programmierumgebung> (1)
- Einkauf (1)
- Empfehlungssystem (1)
- Empirical Studies (1)
- Emulation (1)
- Enhanced Reality (1)
- Enhanced Representation (1)
- Enterprise Information Management (1)
- Enterprise Systems (1)
- Entwickler Profil (1)
- Entwurfsmuster (1)
- Ergonomic Principles (1)
- Erste Hilfe (1)
- European Conference on Modelling and Simulation (1)
- Europäischer Schadensbericht (1)
- Evaluierung (1)
- Eye Tracking (1)
- Eyetracking (1)
- Fabric Simulation (1)
- Facebook Application (1)
- Fahrverhalten (1)
- Fahrzeug (1)
- Farbkalibrierung (1)
- Fault Trees (1)
- Feature Extraction (1)
- Feature Modeling (1)
- Fehlerbaum (1)
- Fiber Tracking (1)
- Fingerprint Recognition (1)
- First aid (1)
- FlexViz (1)
- Food Transportation System (1)
- Foodstuff (1)
- Formal Methods (1)
- Formale Methoden (1)
- Fotoauswahl (1)
- Fragebeantwortung (1)
- Function Words (1)
- GDPR (1)
- GDS (1)
- GPGPU (1)
- GPS (1)
- GReQL2 (1)
- GSM-Standard (1)
- GazeTheWeb (1)
- Gefäßanalyse (1)
- Gefühl (1)
- Gehirn (1)
- Gelände (1)
- Generative Model (1)
- Geocaching (1)
- Gerichteter Graph (1)
- Germany (1)
- Grafikkarte (1)
- Grafikprogrammierung (1)
- Grails (1)
- Grails 1.2 (1)
- Graph Technology (1)
- Graphicsprogramming (1)
- Graphik-Hardware (1)
- Grounded Theory (1)
- Gruppenarbeit (1)
- Hand-based Gestures (1)
- Haskell (1)
- Healthcare institution (1)
- Hindernis (1)
- Horn Clauses (1)
- Human motion (1)
- Human-Computer Interaction (1)
- Hyper Tableau Calculus (1)
- Hypertableaux (1)
- I-messages (1)
- IASON (1)
- IT Guru (1)
- IT Outsourcing (1)
- IT Security (1)
- IT Services (1)
- Image (1)
- Image Processing (1)
- Image Understanding (1)
- Imitation Learning (1)
- Incremental Algorithms (1)
- Industrial-CT (1)
- Informatik (1)
- Information Asset Register (1)
- Information Audit (1)
- Information Capturing Methods (1)
- Information Retrieval (1)
- Information system (1)
- Inpainting-Verfahren (1)
- Intelligent Information Network (1)
- Interactive Video Retrieval (1)
- Internet (1)
- Internet Voting (1)
- Internet of Things (1)
- Interoperability (1)
- Interoperabilität (1)
- JGraLab (1)
- JML (1)
- Java (1)
- Java <Programmiersprache> (1)
- Java Modeling Language (1)
- Java. Programmiersprache (1)
- KRHyper (1)
- Kantenbewerteter Graph (1)
- Kantenverfolgung (1)
- Klassifikation (1)
- Knowledge (1)
- Knowledge Graphs (1)
- Knowledge Sharing (1)
- Kollaboration (1)
- Konturfindung (1)
- Konzept (1)
- Künstliche Intelligenz (1)
- Laser (1)
- Latent Negative (1)
- Leichte Sprache (1)
- Linespace (1)
- Link Prediction (1)
- Linked Data Modeling (1)
- Logik (1)
- Logischer Schluss (1)
- Lokalisation (1)
- MIA (1)
- MPEG-7 (1)
- Machine-Learning (1)
- Machinelles lernen (1)
- MapReduce (1)
- Maschinelles Sehen (1)
- Matching (1)
- MeVisLab (1)
- Mediator framework (1)
- Medical Image Analysis (1)
- Medizinische Bildanalyse (1)
- Medizinische Bildverarbeitung (1)
- Mensch-Maschine-Interaktion (1)
- Merkmalsdetektion (1)
- Merkmalsextrahierung (1)
- Metamodel (1)
- Migration (1)
- Mining (1)
- Mister X (1)
- Mitral Valve (1)
- Mitralklappe (1)
- Mobile Information Systems (1)
- Model-Driven Engineering (1)
- Modellfahrzeug (1)
- Morphologische Operatoren (1)
- Motion Capturing (1)
- Motivation (1)
- Mouse Gestures (1)
- Multi-Agenten-Systeme (1)
- Multi-robot System (1)
- Multiagent System (1)
- Multiagentensysteme (1)
- Multidimensional (1)
- Multimedia Metadata Ontology (1)
- Multimodal Action Recognition (1)
- Multiple Object Tracking (1)
- N-Body Simulation (1)
- N-Körper Simulation (1)
- Native language identification (1)
- Natural Feature Tracking (1)
- Natural Language Processing (1)
- Netzwerk Routing (1)
- Netzwerkanalyse (1)
- OCL <Programmiersprache> (1)
- ODRL (1)
- ONDEX (1)
- OPNET (1)
- OVTK (1)
- Object Recognition (1)
- Objektentfernung (1)
- One-Shot Action Recognition (1)
- Online Community (1)
- Ontologie. Wissensverarbeitung (1)
- Ontology API model (1)
- Ontology alignment (1)
- OpenGL Shading Language (1)
- OpenVDB (1)
- Oracle Generation (1)
- Oraklegenerierung (1)
- PEPPOL (1)
- POIs (1)
- Pan European Public Procurement OnLine (1)
- Path Tracing (1)
- Pattern Recognition (1)
- Personalised Information Systems (1)
- Petri net (1)
- Petri-Netz (1)
- Petrinetz (1)
- Pfadnachverfolgung (1)
- Pfadplanung (1)
- Pfadverfolgung (1)
- Photographie (1)
- Plug in (1)
- Pointing Devices (1)
- Policy Language (1)
- Political Communication (1)
- Politik (1)
- Probabilistic finite automata (1)
- Probability (1)
- Probability propagation nets (1)
- Proceedings (1)
- Process tracing (1)
- Programmierung (1)
- Provenance (1)
- Prozedurale Synthese (1)
- Prädikatenlogik (1)
- Quality assessment system (1)
- Query Expansion (1)
- RDF Graphs (1)
- RDF modeling (1)
- Random Finite Sets (1)
- Raytracing (1)
- ReDSeeDS-Project (1)
- Real-Life Game (1)
- Real-Life Spiel (1)
- Real-Time (1)
- Recommender System (1)
- Reddit (1)
- Reengineering (1)
- Reflections (1)
- Reflektionen (1)
- Regionenlabeling (1)
- Registratur (1)
- Relevance Feedback (1)
- Rendering (1)
- Resource Description Framework (RDF) (1)
- Retina Befundbilder (1)
- Retina Fundus Bilder (1)
- Retina Fundus Images (1)
- Reverse Engineering (1)
- RoboCup (1)
- Robocup 2008 (1)
- Roboter (1)
- Robotik (1)
- Routing Information Protocol (1)
- Routing Information Protocol (RIP) (1)
- Routing Information Protokoll (1)
- Routing Loops (1)
- Routing with Metric based Topology Investigation (RMTI) (1)
- Rückverfolgbarkeit (1)
- SOA (1)
- SPARQL (1)
- STOF Model (1)
- Sattelkraftfahrzeug (1)
- Sattelzug (1)
- Schema Information (1)
- Search engine (1)
- Security (1)
- Security Routing (1)
- Segmentation (1)
- Segmentierung (1)
- Semantic Data (1)
- Semantics (1)
- Service identification (1)
- Service-Identifizierung (1)
- Service-oriented Architectures (SOA) (1)
- Service-orientierte Architektur (1)
- Shader (1)
- Sicherheit Routing (1)
- Simulationswerkzeug (1)
- Smartphone (1)
- Smartphone Applikation (1)
- Social Games (1)
- Social Networking Platforms (1)
- Software (1)
- Software Development (1)
- Software Language (1)
- Software Technology (1)
- Software migration (1)
- Software techniques for object recognition (STOR) (1)
- Software-Migration (1)
- Softwarearchitektur (1)
- Softwareentwicklung (1)
- Softwareergonomie (1)
- Softwaretesting (1)
- Softwarewartung (1)
- Soziales Netzwerk (1)
- Sozialwissenschaftliche Simulation (1)
- Speaker Recognition (1)
- Specification (1)
- Specular (1)
- Spezifikation (1)
- Steuerung (1)
- Stochastic Logic (1)
- Stoffsimulation (1)
- Strassenkreuzung (1)
- Straßenzustand (1)
- Support System (1)
- Survey Research (1)
- Systembiologie (1)
- TAP (1)
- TBox (1)
- TRECVID (1)
- Tableau Calculus (1)
- Taxonomy (1)
- Technologischer Raum (1)
- Tenneco Automotive (1)
- Test Generation (1)
- Testen (1)
- Testgenerierung (1)
- Text (1)
- Text Analysis (1)
- Text Mining (1)
- Text classification (1)
- Texterkennung (1)
- Theorem prover (1)
- Theorembeweiser (1)
- Tokens (1)
- Tool Evaluation (1)
- Traceability (1)
- Tracing (1)
- Tracking-System (1)
- Transferfunction (1)
- Transferfunktion (1)
- Transport (1)
- Type System (1)
- Type system (1)
- Ultraschall (1)
- Ultrasound (1)
- Umfrage in Koblenz (1)
- Unified Modeling Language (UML ) (1)
- Unlink Prediction (1)
- Unsicheres Schließen (1)
- Unterwasser-Pipeline (1)
- Unterwasserfahrzeug (1)
- Unterwasserkabel (1)
- VCD (1)
- VIACOBI (1)
- Vascular analysis (1)
- Vegetation distribution (1)
- Verifikation (1)
- Virtual Company Dossier (1)
- Virtual characters (1)
- Virtuelle Realität (1)
- Visibility Skeleton (1)
- Visual Stimuli Discovery (1)
- Vocabulary Mapping (1)
- Vocabulary Reuse (1)
- Vocabulary Trainer (1)
- Volume Hatching (1)
- WEB (1)
- WLAN Fingerprinting (1)
- WSDL (1)
- WSN (1)
- Wahrscheinlichkeit (1)
- Wahrscheinlichkeitsrechnung (1)
- Wavelet (1)
- Web (1)
- Web Analytics (1)
- Web Analytics Framework (1)
- Web Mining (1)
- Web Ontology Language (OWL) (1)
- Web Science (1)
- Web Services (1)
- Web log (1)
- Web-application framework (1)
- Web-programming technologies (1)
- Weblog (1)
- Website (1)
- Wechselkursänderung (1)
- Werbung (1)
- WiFi Fingerprinting (1)
- Wissensbasis (1)
- Wissensmanagement (1)
- Word-of-Mouth (1)
- World Wide Web 2.0 (1)
- Wrapping (1)
- You-messages (1)
- acceptance (1)
- adaptive resonance theory (1)
- application programming interfaces (1)
- archiving (1)
- artifcial neural networks (1)
- artiffficial neural networks (1)
- artififfcial neural networks (1)
- assessment model (1)
- automated theorem prover (1)
- backpropagation (1)
- benefits (1)
- bias (1)
- blood analysis (1)
- business process management (1)
- by-stander effect (1)
- categorisation (1)
- collaboration (1)
- collaborative technologies (1)
- colour calibration (1)
- concept (1)
- concurrency (1)
- conflict detection (1)
- contexts of use (1)
- core ontologies (1)
- cultural dimensions (1)
- currency exchange rates (1)
- data mining (1)
- data protection (1)
- data warehouse (1)
- deductive (1)
- description logic (1)
- deutsche Hochschulen (1)
- diabetic retinopathy (1)
- diffusion (1)
- directed acyclic graphs (1)
- distinct object identifiers (1)
- distributed information systems (1)
- e-Commerce (1)
- e-learning (1)
- e-service (1)
- e-service quality (1)
- eGovernment (1)
- eSourcing (1)
- eXperience methodology (1)
- edge linking (1)
- estimation of algorithm efficiency (1)
- evaluation (1)
- event model (1)
- event-based systems (1)
- events (1)
- evolution (1)
- eye tracking (1)
- faceted search (1)
- fairness (1)
- finite state automata (1)
- first-order logic (1)
- folksonomies (1)
- functional web testing tools (1)
- gaze information (1)
- gradient method of training weight coefficients (1)
- grassland (1)
- groupwork (1)
- hybrid systems (1)
- hybride Automaten (1)
- hypertableaux (1)
- iCity project (1)
- image processing (1)
- image semantics (1)
- information retrieval (1)
- information system (1)
- jOWL (1)
- knowledge base (1)
- knowledge management system (1)
- knowledge work (1)
- landmarks (1)
- living book (1)
- logistic (1)
- long-living systems (1)
- mPayments (1)
- mathematical model (1)
- medical care (1)
- medical image processing (1)
- metadata formats (1)
- metadata standards (1)
- methodology (1)
- micro-agent (1)
- minimum self-contained graphs (1)
- mobile application (1)
- mobile devices (1)
- mobile facets (1)
- mobile health care (1)
- mobile interaction (1)
- model generation (1)
- model-driven engineering (1)
- modulares System (1)
- morphological operators (1)
- multiagent systems (1)
- multidimensional (1)
- natural language generation (1)
- networks (1)
- neural (1)
- parallel calculations (1)
- path planning (1)
- personal information management (1)
- persönliches Informationsmanagement (1)
- photo selection (1)
- plain language (1)
- points of interest (1)
- policy modelling (1)
- privacy by design (1)
- privacy impact assessment (1)
- privacy protection (1)
- procedural content generation (1)
- public key infrastructure (1)
- question answering (1)
- recurrent (1)
- region labeling (1)
- regression analysis (1)
- regular dag languages (1)
- requirements analysis (1)
- retina fundus images (1)
- rich multimedia presentations (1)
- risk (1)
- robotics (1)
- scaffolded writing (1)
- scene analysis (1)
- security (1)
- semantic annotation (1)
- semantic desktop (1)
- semantischer Desktop (1)
- sequent calculi (1)
- shiq (1)
- simulation (1)
- smartphone app (1)
- social media data (1)
- social object (1)
- software engineering (1)
- summative evaluation (1)
- survey in Koblenz (1)
- tag recommendation (1)
- tagging (1)
- time series (1)
- tool-integration (1)
- traceability (1)
- tracking (1)
- transformation (1)
- unique name assumption (1)
- usability study (1)
- vegetation modeling (1)
- verification (1)
- video games (1)
- virtual goods (1)
- visualization (1)
- web 2.0 (1)
- web-portal medical e-services (1)
- wireless sensor networks (1)
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.
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.
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.
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 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 Silico simulation of biological systems is an important sub area of computational biology (system biology), and becomes more and more an inherent part for research. Therefore, different kinds of software tools are required. At present, a multitude of tools for several areas exists, but the problem is that most of the tools are essentially application specific and cannot be combined. For instance, a software tool for the simulation of biochemical processes is not able to interact with tools for the morphology simulation and vice versa. In order to obtain realistic results with computer-aided simulations it is important to regard the biological system in its entirety. The objective is to develop a software framework, which provides an interface structure to combine existing simulation tools, and to offer an interaction between all affiliated systems. Consequently, it is possible to re-use existing models and simulation programs. Additionally, dependencies between those can be defined. The system is designed to interoperate as an extendable architecture for various tools. The thesis shows the usability and applicability of the software and discusses potential improvements.
Knowledge compilation is a common technique for propositional logic knowledge bases. The idea is to transform a given knowledge base into a special normal form ([MR03],[DH05]), for which queries can be answered efficiently. This precompilation step is very expensive but it only has to be performed once. We propose to apply this technique to knowledge bases defined in Description Logics. For this, we introduce a normal form, called linkless concept descriptions, for ALC concepts. Further we present an algorithm, based on path dissolution, which can be used to transform a given concept description into an equivalent linkless concept description. Finally we discuss a linear satisfiability test as well as a subsumption test for linkless concept descriptions.
The term "Augmented Reality (AR)" denotes the superposition of additional virtual objects and supplementary information over real images. The joint project Enhanced Reality (ER)1 aims at a generic AR-system. The ER-project is a cooperation of six different research groups of the Department of Computer Science at the University of Koblenz-Landau. According to Ronald Azuma an AR-system combines real and virtual environments, where the real and virtual objects are registered in 3-D, and it provides interactivity in real time [Azu97]. Enhanced Reality extends Augmented Reality by requiring the virtual objects to be seamlessly embedded into the real world as photo-realistic objects according to the exact lighting conditions. Furthermore, additional information supplying value-added services may be displayed and interaction of the user may even be immersive. The short-term goal of the ER-project is the exploration of ER-fundamentals using some specific research scenarios; the long-term goal is the development of a component-based ER-framework for the creation of ER-applications for arbitrary application areas. ER-applications are developed as single-user applications for users who are moving in a real environment and are wearing some kind of visual output device like see-through glasses and some mobile end device. By these devices the user is able to see reality as it is, but he can also see the virtual objects and the additional information about some value-added service. Furthermore he might have additional devices whereby he can interact with the available virtual objects. The development of a generic framework for ER-applications requires the definition of generic components which are customizable and composable to build concrete applications and it requires a homogeneous data model which supports all components equally well. The workgroup "Software Technology"2 is responsible for this subproject. This report gives some preliminary results concerning the derivation of a component-based view of ER. There are several augmented reality frameworks like ARVIKA, AMIRE, DWARF, MORGAN, Studierstube and others which offer some support for the development of AR-applications. All of them ease the use of existing subsystems like AR-Toolkit, OpenGL and others and leverage the generation process for realistic systems by making efficient use of those subsystems. Consequently, they highly rely on them.
Probability propagation nets
(2007)
A class of high level Petri nets, called "probability propagation nets", is introduced which is particularly useful for modeling probability and evidence propagation. These nets themselves are well suited to represent the probabilistic Horn abduction, whereas specific foldings of them will be used for representing the flows of probabilities and likelihoods in Bayesian networks.
In this paper we describe a series of projects on location based and personalised information systems. We start wit a basic research project and we show how we came with the help of two other more application oriented project to a product. This is developed by a consortium of enterprises and it already is in use in the city of Koblenz.
This paper describes the development of security requirements for non-political Internet voting. The practical background is our experience with the Internet voting within the Gesellschaft für Informatik (GI - Informatics Society) 2004 and 2005. The theoretical background is the international state-of-the-art of requirements about electronic voting, especially in the US and in Europe. A focus of this paper is on the user community driven standardization of security requirements by means of a Protection Profile of the international Common Criteria standard.
In this paper we describe a network for distributing personalized information within a pervasive university. We discuss the system architecture of our Bluetooth-based CampusNews-system, both, from the administrator and the user viewpoint. We furthermore present first statistical data about the usage of the partial installation at the Koblenz campus together with an outlook to future work.
The thesis develops and evaluates a hypothetical model of the factors that influence user acceptance of weblog technology. Previous acceptance studies are reviewed, and the various models employed are discussed. The eventual model is based on the technology acceptance model (TAM) by Davis et al. It conceptualizes and operationalizes a quantitative survey conducted by means of an online questionnaire, strictly from a user perspective. Finally, it is tested and validated by applying methods of data analysis.
This paper shows how multiagent systems can be modeled by a combination of UML statecharts and hybrid automata. This allows formal system specification on different levels of abstraction on the one hand, and expressing real-time system behavior with continuous variables on the other hand. It is not only shown how multi-robot systems can be modeled by a combination of hybrid automata and hierarchical state machines, but also how model checking techniques for hybrid automata can be applied. An enhanced synchronization concept is introduced that allows synchronization taking time and avoids state explosion to a certain extent.
Computed tomography (CT) and magnetic resonance imaging (MRI) in the medical area deliver huge amounts of data, which doctors have to handle in a short time. These data can be visualised efficiently with direct volume rendering. Consequently most direct volume rendering applications on the market are specialised on medical tasks or integrated in medical visualisa- tion environments. Highly evolved applications for tasks like diagnosis or surgery simulation are available in this area. In the last years, however, another area is making increasing use of com- puted tomography. Companies like phoenix |x-ray, founded in 1999 pro- duce CT-scanners especially dedicated to industrial applications like non destructive material testing (NDT). Of course an application like NDT has different demands on the visualisation than a typical medical application. For example a typical task for non destructive testing would be to high- light air inclusions (pores) in a casting. These inclusions usually cover a very small area and are very hard to classify only based on their density value as this would also highlight the air around the casting. This thesis presents multiple approaches to improve the rendering of in- dustrial CT data, most of them based on higher dimensional transfer func- tions. Therefore the existing volume renderer application of VRVis was extended with a user interface to create such transfer functions and exist- ing render modes were adapted to profit from the new transfer functions. These approaches are especially suited to improve the visualisation of sur- faces and material boundaries as well as pores. The resulting renderings make it very easy to identify these features while preserving interactive framerates.
SOA-Security
(2007)
This paper is a part of the ASG project (Adaptive Services Grid) and addresses some IT security issues of service oriented architectures. It defines a service-oriented security concept, it explores the SOA security challenge, it describes the existing WS-Security standard, and it undertakes a first step into a survey on best practice examples. In particular, the ASG middleware platform technology (JBossWS) is analyzed with respect to its ability to handle security functions.
Networked RDF graphs
(2007)
Networked graphs are defined in this paper as a small syntactic extension of named graphs in RDF. They allow for the definition of a graph by explicitly listing triples as well as by SPARQL queries on one or multiple other graphs. By this extension it becomes possible to define a graph including a view onto other graphs and to define the meaning of a set of graphs by the way they reference each other. The semantics of networked graphs is defined by their mapping into logic programs. The expressiveness and computational complexity of networked graphs, varying by the set of constraints imposed on the underlying SPARQL queries, is investigated. We demonstrate the capabilities of networked graphs by a simple use case.
Hyper tableaux with equality
(2007)
In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for paramodulation are drawn (only) from a set of positive unit clauses, the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many redundancy elimination techniques known from superposition theorem proving. Our main results are soundness and completeness, but we briefly describe the implementation, too.
UML models and OWL ontologies constitute modeling approaches with different strength and weaknesses that make them appropriate for use of specifying different aspects of software systems. In particular, OWL ontologies are well suited to specify classes using an expressive logical language with highly flexible, dynamic and polymorphic class membership, while UML diagrams are much more suitable for specifying not only static models including classes and associations, but also dynamic behavior. Though MOF based metamodels and UML profiles for OWL have been proposed in the past, an integrated use of both modeling approaches in a coherent framework has been lacking so far. We present such a framework, TwoUse, for developing integrated models, comprising the benefits of UML models and OWL ontologies
In this paper we describe a network for distributing personalized Information in a metropolitan area. We discuss the system architecture of our Bluetooth-based information system as well as the reasoning process that fits users" needs with potential messages. We furthermore present our findings on parallelizing Bluetooth connection setup and performance.
Semantic descriptions of non-textual media available on the web can be used to facilitate retrieval and presentation of media assets and documents containing them. While technologies for multimedia semantic descriptions already exist, there is as yet no formal description of a high quality multimedia ontology that is compatible with existing (semantic) web technologies. We explain the complexity of the problem using an annotation scenario. We then derive a number of requirements for specifying a formal multimedia ontology, including: compatibility with MPEG-7, embedding in foundational ontologies, and modularisation including separation of document structure from domain knowledge. We then present the developed ontology and discuss it with respect to our requirements.
Generalized methods for automated theorem proving can be used to compute formula transformations such as projection elimination and knowledge compilation. We present a framework based on clausal tableaux suited for such tasks. These tableaux are characterized independently of particular construction methods, but important features of empirically successful methods are taken into account, especially dependency directed backjumping and branch local operation. As an instance of that framework an adaption of DPLL is described. We show that knowledge compilation methods can be essentially improved by weaving projection elimination partially into the compilation phase.
This paper offers an informal overview and discussion on first order predicate logic reasoning systems together with a description of applications which are carried out in the Artificial Intelligence Research Group of the University in Koblenz. Furthermore the technique of knowledge compilation is shortly introduced.
The E-KRHyper system is a model generator and theorem prover for first-order logic with equality. It implements the new E-hyper tableau calculus, which integrates a superposition-based handling of equality into the hyper tableau calculus. E-KRHyper extends our previous KRHyper system, which has been used in a number of applications in the field of knowledge representation. In contrast to most first order theorem provers, it supports features important for such applications, for example queries with predicate extensions as answers, handling of large sets of uniformly structured input facts, arithmetic evaluation and stratified negation as failure. It is our goal to extend the range of application possibilities of KRHyper by adding equality reasoning.
We introduce linear expressions for unrestricted dags (directed acyclic graphs) and finite deterministic and nondeterministic automata operating on them. Those dag automata are a conservative extension of the Tu,u-automata of Courcelle on unranked, unordered trees and forests. Several examples of dag languages acceptable and not acceptable by dag automata and some closure properties are given.
Zahlreiche Studien belegen, dass menschliche Bewegungen Informationen über den Akteur in sich bergen. Beobachter sind daher in der Lage, Dinge wie Persönlichkeit, Geschlecht und Gefühlslage allein aus Bewegungen von Menschen zu erkennen. Um dem Ziel nach glaubwürdigen und realistischen virtuellen Charakteren näher zu kommen, verbesserte sich in den letzten Jahren vorwiegend das Aussehen der Charaktere. Dank moderner Techniken und einer rapiden Entwicklung der Computer Hardware können heute visuell extrem realistische Charaktere in virtuellen Echtzeitumgebungen dargestellt werden. Trotz ihrer visuellen Qualität werden sie jedoch in interaktiven Umgebungen häufig als mechanisch wahrgenommen. Diese Störung der Illusion, einem lebendigen, Menschen ähnlichem Lebewesen gegen über zu stehen ist in einem mangelndem menschlichen Verhalten des virtuellen Charakters begründet. Daher können ausdrucksvolle Bewegungen, die einen emotionalen Zustand des Charakters vermitteln, dazu verhelfen dem Menschen ähnlichere und daher glaubwürdigere Charaktere zu realisieren. Im Rahmen dieser Diplomarbeit wird die Umsetzbarkeit eines Systems zur automatischen Generierung emotional expressiver Charakter Animationen untersucht. Übliche Techniken zur Erstellung von Animationen sind sehr aufwendig und zeitintensiv. Um alle möglichen Variationen von Bewegungen in einer interaktiven Umgebung zu erstellen kommen solche Ansätze daher nicht in Frage. Um interaktive Charakter zu ermöglichen, welche in der Lage sind ihre Gefühle zum Ausdruck zu bringen, wird daher diese Problematik im Zuge dieser Diplomarbeit behandelt werden. Einschlägige Literatur aus Forschungsgebieten, welche sich mit Emotionen und Bewegungen befassen werden im Rahmen dieser Arbeit untersucht. Eigenschaften, anhand derer Menschen Emotionen in Bewegungen erkennen, werden technisch in einem Animationssystem umgesetzt, um aus neutralen Animationen emotionale Bewegungen zu generieren. Abschliessend werden die erstellten Ergebnisanimationen in Tests ausgewertet in Bezug auf Erkennbarkeit der Emotionen und Qualität der Ergebnisse.
This volume contains those research papers presented at the Second International Conference on Tests and Proofs (TAP 2008) that were not included in the main conference proceedings. TAP was the second conference devoted to the convergence of proofs and tests. It combines ideas from both areas for the advancement of software quality. To prove the correctness of a program is to demonstrate, through impeccable mathematical techniques, that it has no bugs; to test a program is to run it with the expectation of discovering bugs. On the surface, the two techniques seem contradictory: if you have proved your program, it is fruitless to comb it for bugs; and if you are testing it, that is surely a sign that you have given up on any hope of proving its correctness. Accordingly, proofs and tests have, since the onset of software engineering research, been pursued by distinct communities using rather different techniques and tools. And yet the development of both approaches leads to the discovery of common issues and to the realization that each may need the other. The emergence of model checking has been one of the first signs that contradiction may yield to complementarity, but in the past few years an increasing number of research efforts have encountered the need for combining proofs and tests, dropping earlier dogmatic views of their incompatibility and taking instead the best of what each of these software engineering domains has to offer. The first TAP conference (held at ETH Zurich in February 2007) was an attempt to provide a forum for the cross-fertilization of ideas and approaches from the testing and proving communities. For the 2008 edition we found the Monash University Prato Centre near Florence to be an ideal place providing a stimulating environment. We wish to sincerely thank all the authors who submitted their work for consideration. And we would like to thank the Program Committee members as well as additional referees for their great effort and professional work in the review and selection process. Their names are listed on the following pages. In addition to the contributed papers, the program included three excellent keynote talks. We are grateful to Michael Hennell (LDRA Ltd., Cheshire, UK), Orna Kupferman (Hebrew University, Israel), and Elaine Weyuker (AT&T Labs Inc., USA) for accepting the invitation to address the conference. Two very interesting tutorials were part of TAP 2008: "Parameterized Unit Testing with Pex" (J. de Halleux, N. Tillmann) and "Integrating Verification and Testing of Object-Oriented Software" (C. Engel, C. Gladisch, V. Klebanov, and P. Rümmer). We would like to express our thanks to the tutorial presenters for their contribution. It was a team effort that made the conference so successful. We are grateful to the Conference Chair and the Steering Committee members for their support. And we particularly thank Christoph Gladisch, Beate Körner, and Philipp Rümmer for their hard work and help in making the conference a success. In addition, we gratefully acknowledge the generous support of Microsoft Research Redmond, who financed an invited speaker.
The University of Koblenz-Landau would like to apply for participation in the RoboCup Mixed Reality League in Suzhou, China 2008. Our team is composed of ten team members and two supervisors. All members are graduate students of Computational Visualistics. Our supervisors are Ph.D. candidates currently researching in the working groups of artificial intelligence and computer graphics.
Social networking platforms as creativity fostering systems: research model and exploratory study
(2008)
Social networking platforms are enabling users to create their own content, share this content with anyone they invite and organize connections with existing or new online contacts. Within these electronic environments users voluntarily add comments on virtual boards, distribute their search results or add information about their expertise areas to their social networking profiles and thereby share it with acquaintances, friends and increasingly even with colleagues in the corporate world. As a result, it is most likely that the underlying knowledge sharing processes result in many new and creative ideas. The objective of our research therefore is to understand if and how social social networking platforms can enforce creativity. In addition, we look at how these processes could be embedded within the organizational structures that influence innovative knowledge sharing behavior. The basis for our research is a framework which focuses on the relations between intrinsic motivation, creativity and social networking platforms. First results of our empirical investigation of a social software platform called "StudiVZ.net" proved that our two propositions are valid.
Probability propagation nets
(2008)
In der vorliegenden Arbeit wird eine Petri-Netz-Repräsentation für die Propagation von Wahrscheinlichkeiten und Evidenzen (Likelihoods) vorgestellt und auf probabilistische Horn-Abduktion sowie Fehlerbäume und Bayes-Netze angewendet. Diese sogenannten Wahrscheinlichkeits-Propagations-Netze (probability propagation nets) machen Propagations-Prozesse transparent, indem sie strukturelle und dynamische Aspekte in einer homogenen Darstellung vereinen. Anhand populärer Beispiele wird verdeutlicht, dass Wahrscheinlichkeits-Propagations-Netze die Propagations-Prozesse - besonders im Hinblick auf die Bayes-Netz-Algorithmik - anschaulich darstellen und gut nachvollziehbar machen, so dass sie sich für die Analyse und Diagnose probabilistischer Modelle eignen. Durch die Repräsentation von Fehlerbäumen mit Wahrscheinlichkeits-Propagations-Netzen können diese Vorzüge auf die Modellierung technischer Systeme übertragen werden.
Querying for meta knowledge
(2008)
The Semantic Web is based on accessing and reusing RDF data from many different sources, which one may assign different levels of authority and credibility. Existing Semantic Web query languages, like SPARQL, have targeted the retrieval, combination and reuse of facts, but have so far ignored all aspects of meta knowledge, such as origins, authorship, recency or certainty of data, to name but a few. In this paper, we present an original, generic, formalized and implemented approach for managing many dimensions of meta knowledge, like source, authorship, certainty and others. The approach re-uses existing RDF modeling possibilities in order to represent meta knowledge. Then, it extends SPARQL query processing in such a way that given a SPARQL query for data, one may request meta knowledge without modifying the query proper. Thus, our approach achieves highly flexible and automatically coordinated querying for data and meta knowledge, while completely separating the two areas of concern.
Die automatische Detektion der Lage und Ausrichtung von Unterwasser-Kabeln oder -Pipelines in Kamerabildern ermöglicht es, Unterwasserfahrzeuge autonome Kontrollfahrten durchführen zu lassen. Durch Pflanzenwuchs auf und in der Nähe von Kabeln bzw. Pipelines wird deren visuelle Erfassung jedoch erschwert: Die Bestimmug der Lage über die Detektion von Kanten mit anschließender Linien-Extraktion schlägt oft fehl. Probabilistische Ansätze sind hier den deterministischen überlegen. Durch die Modellierung von Wahrscheinlichkeiten kann trotz geringer Anzahl von extrahierten Merkmalen eine Aussage über den Zustand des Systems getroffen werden. Diese Arbeit stellt ein neues auf Partikelfiltern basierendes Tracking-System für die Verfolgung von Kabeln und Pipelines in Bildsequenzen vor. Umfangreiche Experimente auf realistischen Unterwasser-Videos zeigen die Robustheit und Performanz des gewählten Ansatzes sowie Vorteile gegenüber vorangegangenen Arbeiten.
Öffentliche elektronische Beschaffung (eProcurement), bzw. strategischer elektronischer Einkauf (eSourcing), sind mit hoher Wahrscheinlichkeit Thema sobald eGovernment Experten aufeinander treffen. So ist es nicht überraschend, dass eProcurement im aktuellen Aktionsplan der EU als "high-impact service" eingestuft wurde. Dies lässt sich zum Großteil durch den großen Einfluss vom öffentlichen Einkauf auf die Staatskasse erklären. So macht eProcurement in der Regel bis zu 20% des BIP aus und beherbergt somit ein enormes Einsparpotenzial. Dieses Potenzial liegt zum Teil im gemeinsamen Europäischen Wirtschaftsraum, da effizientes länderübergreifendes eSourcing neue Möglichkeiten für Einkäufer sowie Lieferanten eröffnen kann. Um diese Möglichkeiten ausschöpfen zu können, müssen Prozesse und Tools in der Lage sein, miteinander zu kommunizieren, sich aufeinander abzustimmen oder transferierbar sein. In einem Wort, sie müssen interoperabel sein. In vielen wichtigen Bereichen ist Interoperabilität sehr weit fortgeschritten, in anderen hingegen muss noch viel verändert werden. Daher ist es von wesentlicher Bedeutung Interoperabilitätsanforderungen zu definieren, sowie den aktuellen Forschungs- und Entwicklungsstand zu evaluieren.
Computers and especially computer networks have become an important part of our everyday life. Almost every device we use is equipped with a computer or microcontroller. Recent technology has even boosted this development by miniaturization of the size of microcontrollers. These are used to either process or collect data. Miniature senors may sense and collect huge amounts of information coming from nature, either from environment or from our own bodies. To process and distribute the data of these sensors, wireless sensor networks (WSN) have been developed in the last couple of years. Several microcontrollers are connected over a wireless connection and are able to collect, transmit and process data for various applications. Today, there are several WSN applications available, such as environment monitoring, rescue operations, habitat monitoring and smart home applications. The research group of Prof. Elaine Lawrence at the University of Technology, Sydney (UTS) is focusing on mobile health care with WSN. Small sensors are used to collect vital data. This data is sent over the network to be processed at a central device such as computer, laptop or handheld device. The research group has developed several prototypes of mobile health care. This thesis will deal with enhancing and improving the latest prototype based on CodeBlue, a hardware and software framework for medical care.
In dieser Dissertation wird eine Verfahrensweise für die formale Spezifikation und Verifikation von Benutzerschnittstellen unter Sicherheitsaspekten vorgestellt. Mit dieser Verfahrensweise können beweisbar sichere Benutzerschnittstellen realisiert werden. Die Arbeit besteht aus drei Teilen. Im ersten Teil wird eine Methodologie für die formale Beschreibung von Mensch-Maschine-Interaktion entwickelt. Im zweiten Teil werden gängige Computersicherheitskonzepte für die Mensch-Maschine-Interaktion angepasst und mit den im ersten Teil entwickelten Methoden formalisiert. Dabei wird ein generisches formales Modell von Mensch-Maschine-Interaktion erstellt. Im dritten Teil wird die Methodologie, die in den ersten beiden Teilen entwickelt wurde, an einem sicheren Email-Client als exemplarischen Anwendungsprogramm demonstriert.
Weltweit kann im letzten Jahrzehnt auf eine rasch zunehmende Akzeptanz des Internets als Informationsplattform zurückgeblickt werden. Grundlegende Änderungen fanden sowohl im privaten als auch im öffentlichen Sektor statt. Im Zuge dessen wurde die aktive Beteiligung von Bürgern in politische Meinungsbildungsprozesse mehr und mehr elektronisch unterstützt. Die Erwartungen an die neue Technologie steigerten sich in die Annahme, dass Informations- und Kommunikationstechnologien (IKT) die Bürgerbeteiligung verbessern und die Politikverdrossenheit mindern können. Aus diesen Erwartungen entwickelten sich einige E-Partizipationsprojekte in Deutschland. Außerdem wurde die "Initiative eParticipation" ins Leben gerufen, die in Bezug auf E-Partizipation Politik und Verwaltungen stark anregte, den Entscheidungsprozess mit Hilfe von internetgestützten Beteiligungspraktiken zu stärken. Diese Arbeit besteht aus zwei Hauptteilen. Im ersten Teil werden Definitionen der kritischen Begriffe präsentiert. Außerdem wird die Position von E-Partizipation innerhalb der Dimension des E-Business aufgezeigt. Um E-Partizipation zu erläutern, werden zuerst Grundlagen der klassischen Bürgerbeteiligung erklärt. Es wird gezeigt, dass sich auch die klassische Bürgerbeteiligung in einem Veränderungsprozess befindet, dessen Ursache nicht nur der Einsatz von IKT ist. Nachfolgend wird ein Rahmenwerk präsentiert, welches das Spektrum von E-Partizipation charakterisiert. Die Europäische Union fördert die Umsetzung von E-Partizipation. Koblenz soll da keine Ausnahme bilden. Aber wie ist die momentane Situation in Koblenz? Um diese Frage zu beantworten wird der gegenwärtige Zustand untersucht. Dazu wurde eine Umfrage unter den Bürgern der Stadt entwickelt, durchgeführt und ausgewertet. Dies ist der zweite Hauptteil dieser Arbeit.
CAMPUS NEWS - artificial intelligence methods combined for an intelligent information network
(2008)
In this paper we describe a network for distributing personalised information with the usage of artificial intelligence methods. Reception of this information should be possible with everyday mobile equipment. Intelligent filtering and spam protection aim at integrating this technology into our environment. Information on the system architecture and usage of the installation are also presented.
Semantic desktop environments aim at improving the effectiveness and efficiency of users carrying out daily tasks within their personal information management infrastructure (PIM). They support the user by transferring and exploiting the explicit semantics of data items across different PIM applications. Whether such an approach does indeed reach its aim of facilitating users" life and—if so—to which extent, however, remains an open question that we address in this paper with the first summative evaluation of a semantic desktop approach. We approach the research question exploiting our own semantic desktop infrastructure, X-COSIM. As data corpus, we have used over 100 emails and 50 documents extracted from the organizers of a conference-like event at our university. The evaluation has been carried out with 18 subjects. We have developed a test environment to evaluate COSIMail and COSIFile, two semantic PIM applications based on X-COSIM. As result, we have found a significant improvement for typical PIM tasks compared to a standard desktop environment.
The STOR project aims at the development of a scientific component system employing models and knowledge for object recognition in images. This interim report elaborates on the requirements for such a component system, structures the application area by identifying a large set of basic operations, and shows how a set of appropriate data structures and components can be derived. A small case studies exemplifies the approach.
Hybrid systems are the result of merging the two most commonly used models for dynamical systems, namely continuous dynamical systems defined by differential equations and discrete-event systems defined by automata. One can view hybrid systems as constrained systems, where the constraints describe the possible process flows, invariants within states, and transitions on the one hand, and to characterize certain parts of the state space (e.g. the set of initial states, or the set of unsafe states) on the other hand. Therefore, it is advantageous to use constraint logic programming (CLP) as an approach to model hybrid systems. In this paper, we provide CLP implementations, that model hybrid systems comprising several concurrent hybrid automata, whose size is only straight proportional to the size of the given system description. Furthermore, we allow different levels of abstraction by making use of hierarchies as in UML statecharts. In consequence, the CLP model can be used for analyzing and testing the absence or existence of (un)wanted behaviors in hybrid systems. Thus in summary, we get a procedure for the formal verification of hybrid systems by model checking, employing logic programming with constraints.
The lack of a formal event model hinders interoperability in distributed event-based systems. Consequently, we present in this paper a formal model of events, called F. The model bases on an upper-level ontology and pro-vides comprehensive support for all aspects of events such as time and space, objects and persons involved, as well as the structural aspects, namely mereological, causal, and correlational relationships. The event model provides a flexible means for event composition, modeling of event causality and correlation, and allows for representing different interpretations of the same event. The foundational event model F is developed in a pattern-oriented approach, modularized in different ontologies, and can be easily extended by domain specifific ontologies.
Avoidance of routing loops
(2009)
We introduce a new routing algorithm which can detect routing loops by evaluating routing updates more thoroughly. Our new algorithm is called Routing with Metric based Topology Investigation (RMTI), which is based on the simple Routing Information Protocol (RIP) and is compatible to all RIP versions. In case of a link failure, a network can reorganize itself if there are redundant links available. Redundant links are only available in a network system like the internet if the topology contains loops. Therefore, it is necessary to recognize and to prevent routing loops. A routing loop can be seen as a circular trace of a routing update information which returns to the same router, either directly from the neighbor router or via a loop topology. Routing loops could consume a large amount of network bandwidth and could impact the endtoend performance of the network. Our RMTI approach is capable to improve the efficiency of Distance Vector Routing.
Software is vital for modern society. The efficient development of correct and reliable software is of ever-growing importance. An important technique to achieve this goal is deductive program verification: the construction of logical proofs that programs are correct. In this thesis, we address three important challenges for deductive verification on its way to a wider deployment in the industry: 1. verification of thread-based concurrent programs 2. correctness management of verification systems 3. change management in the verification process. These are consistently brought up by practitioners when applying otherwise mature verification systems. The three challenges correspond to the three parts of this thesis (not counting the introductory first part, providing technical background on the KeY verification approach). In the first part, we define a novel program logic for specifying correctness properties of object-oriented programs with unbounded thread-based concurrency. We also present a calculus for the above logic, which allows verifying actual Java programs. The calculus is based on symbolic execution resulting in its good understandability for the user. We describe the implementation of the calculus in the KeY verification system and present a case study. In the second part, we provide a first systematic survey and appraisal of factors involved in reliability of formal reasoning. We elucidate the potential and limitations of self-application of formal methods in this area and give recommendations based on our experience in design and operation of verification systems. In the third part, we show how the technique of similarity-based proof reuse can be applied to the problems of industrial verification life cycle. We address issues (e.g., coping with changes in the proof system) that are important in verification practice, but have been neglected by research so far.