Filtern
Erscheinungsjahr
Dokumenttyp
- Ausgabe (Heft) zu einer Zeitschrift (84) (entfernen)
Sprache
- Englisch (84) (entfernen)
Schlagworte
- Bluetooth (4)
- ontology (4)
- Knowledge Compilation (3)
- computer clusters (3)
- Campus Information System (2)
- E-KRHyper (2)
- Equality (2)
- Linked Open Data (2)
- OWL (2)
- Ontology (2)
- Petri-Netze (2)
- Semantic Web (2)
- Theorem Proving (2)
- University (2)
- artificial neural networks (2)
- classification (2)
- constraint logic programming (2)
- mobile phone (2)
- multimedia metadata (2)
- parallel algorithms (2)
- probability propagation nets (2)
- risk (2)
- social media (2)
- ABox (1)
- Adaptive Services Grid (ASG) (1)
- Amazon Mechanical Turks (1)
- Augmented Reality (1)
- Automated Theorem Proving (1)
- Automated Theorem Proving Systems (1)
- Bayes Procedures (1)
- COVID-19 (1)
- Calculus (1)
- Cloud Computing (1)
- Computer Supported Cooperative Work (1)
- Conference (1)
- Context-aware processes (1)
- Core Ontology on Multimedia (1)
- Core Ontology on Multimedia (COMM) (1)
- Creativity (1)
- Crowdsourcing (1)
- DPLL procedure (1)
- Description Logic (1)
- Description Logics (1)
- Discussion Forums (1)
- Distributed process execution (1)
- E-KRHyper theorem prover (1)
- E-government (1)
- E-services (1)
- Enhanced Reality (1)
- Enterprise Systems (1)
- Generative Model (1)
- Graph Technology (1)
- Healthcare institution (1)
- Heimarbeit (1)
- Horn Clauses (1)
- Hyper Tableau Calculus (1)
- IASON (1)
- IT Outsourcing (1)
- IT Security (1)
- IT Services (1)
- Image (1)
- Intelligent Information Network (1)
- Internet (1)
- Internet Voting (1)
- KRHyper (1)
- Knowledge Sharing (1)
- Linked Data Modeling (1)
- MIA (1)
- MPEG-7 (1)
- Mixed method (1)
- Mobile Information Systems (1)
- Model-Driven Engineering (1)
- Multi-robot System (1)
- Multiagent System (1)
- Multimedia Metadata Ontology (1)
- Neuronales Netz (1)
- ODRL (1)
- Object Recognition (1)
- Online Community (1)
- Ontology alignment (1)
- POIs (1)
- Personalised Information Systems (1)
- Petri Nets (1)
- Petri net (1)
- Petrinetz (1)
- Probability (1)
- Probability propagation nets (1)
- Process tracing (1)
- Propagation (1)
- Quality assessment system (1)
- RDF (1)
- RDF Graphs (1)
- RDF modeling (1)
- Railway Research (1)
- Railway Research Topics (1)
- Railway Safety (1)
- Railway Safety Research (1)
- ReDSeeDS-Project (1)
- Resource Description Framework (RDF) (1)
- Robocup 2008 (1)
- Routing Information Protocol (RIP) (1)
- Routing Loops (1)
- Routing with Metric based Topology Investigation (RMTI) (1)
- SPARQL (1)
- Schema Information (1)
- Search engine (1)
- Security (1)
- Semantics (1)
- Service-oriented Architectures (SOA) (1)
- Social Networking Platforms (1)
- Software Development (1)
- Software techniques for object recognition (STOR) (1)
- Stochastic Logic (1)
- Support System (1)
- Survey Research (1)
- TAP (1)
- TBox (1)
- Tableau Calculus (1)
- Telearbeit (1)
- Theorem prover (1)
- Tokens (1)
- Traceability (1)
- UML (1)
- Umfrage (1)
- Unified Modeling Language (UML ) (1)
- Vocabulary Mapping (1)
- Vocabulary Reuse (1)
- Web Ontology Language (OWL) (1)
- Website (1)
- Wechselkursänderung (1)
- Werbung (1)
- Word-of-Mouth (1)
- XML (1)
- adaptive resonance theory (1)
- application programming interfaces (1)
- artifcial neural networks (1)
- artiffficial neural networks (1)
- artififfcial neural networks (1)
- assessment model (1)
- blood analysis (1)
- business process management (1)
- categorisation (1)
- core ontologies (1)
- currency exchange rates (1)
- delivery drone (1)
- design thinking (1)
- digital workplace (1)
- directed acyclic graphs (1)
- drone (1)
- e-Commerce (1)
- e-learning (1)
- e-service (1)
- e-service quality (1)
- entrepreneurial design thinking (1)
- entrepreneurial thinking (1)
- entrepreneurship education (1)
- estimation of algorithm efficiency (1)
- event model (1)
- event-based systems (1)
- events (1)
- faceted search (1)
- finite state automata (1)
- first-order logic (1)
- gaze information (1)
- governance (1)
- gradient method of training weight coefficients (1)
- hybrid automata (1)
- hybrid systems (1)
- hybrid work (1)
- iCity project (1)
- image processing (1)
- image semantics (1)
- information system (1)
- knowledge management system (1)
- knowledge work (1)
- living book (1)
- mathematical model (1)
- media competence model (1)
- metadata formats (1)
- metadata standards (1)
- methodology (1)
- minimum self-contained graphs (1)
- mobile application (1)
- mobile devices (1)
- mobile facets (1)
- mobile interaction (1)
- model generation (1)
- multi-agent systems (1)
- parallel calculations (1)
- personal information management (1)
- persönliches Informationsmanagement (1)
- points of interest (1)
- privacy and personal data (1)
- privacy competence model (1)
- privacy protection (1)
- public key infrastructure (1)
- regression analysis (1)
- regular dag languages (1)
- remote work (1)
- rich multimedia presentations (1)
- risks (1)
- scene analysis (1)
- security awareness (1)
- semantic annotation (1)
- semantic desktop (1)
- semantics (1)
- semantischer Desktop (1)
- sequent calculi (1)
- social media data (1)
- social object (1)
- social simulation (1)
- summative evaluation (1)
- tagging (1)
- teams (1)
- technology acceptance model (1)
- time series (1)
- tracking (1)
- virtual goods (1)
- visualization (1)
- web-portal medical e-services (1)
- work from anywhere (1)
- work from home (1)
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.
This paper describes the robots TIAGo and Lisa used by
team homer@UniKoblenz of the University of Koblenz-Landau, Germany,
for the participation at the RoboCup@Home 2019 in Sydney,
Australia. We ended up first at RoboCup@Home 2019 in the Open Platform
League and won the competition in our league now three times
in a row (four times in total) which makes our team the most successful
in RoboCup@Home. We demonstrated approaches for learning from
demonstration, touch enforcing manipulation and autonomous semantic
exploration in the finals. A special focus is put on novel system components
and the open source contributions of our team. We have released
packages for object recognition, a robot face including speech synthesis,
mapping and navigation, speech recognition interface, gesture recognition
and imitation learning. The packages are available (and new packages
will be released) on http://homer.uni-koblenz.de.
This paper describes the robots TIAGo and Lisa used by team homer@UniKoblenz of the University of Koblenz-Landau, Germany, for the participation at the RoboCup@Home 2018 in Montreal, Canada. Further this paper serves as qualification material for the RoboCup-@Home participation in 2018. A special focus is put on novel system components and the open source contributions of our team. This year the team from Koblenz won the biggest annual scientianc robot competition in Montreal in the RoboCup@Home Open Platform track for the third time and also won the RoboCup@Home German Open for the second time. As a research highlight a novel symbolic imitation learning approach was demonstrated during the annals. The TIAGo robotic research platform was used for the first time by the team. We have released packages for object recognition, a robot face including speech synthesis, mapping and navigation, speech recognition interface via android and a GUI. The packages are available (and new packages will be released) on http://wiki.ros.org/agas-ros-pkg. Further information can be found on our project page http://homer.uni-koblenz.de.
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.
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.
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.
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.
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.
E-KRHyper is a versatile theorem prover and model generator for firstorder logic that natively supports equality. Inequality of constants, however, has to be given by explicitly adding facts. As the amount of these facts grows quadratically in the number of these distinct constants, the knowledge base is blown up. This makes it harder for a human reader to focus on the actual problem, and impairs the reasoning process. We extend E-Hyper- underlying E-KRhyper tableau calculus to avoid this blow-up by implementing a native handling for inequality of constants. This is done by introducing the unique name assumption for a subset of the constants (the so called distinct object identifiers). The obtained calculus is shown to be sound and complete and is implemented into the E-KRHyper system. Synthetic benchmarks, situated in the theory of arrays, are used to back up the benefits of the new calculus.
Artificial intelligence (AI) is of rising importance in these days. AI is increasingly used in various company fields. Nonetheless, no high-quality scientific sources could be found stating the use of AI in the field of leadership. This research gap is addressed with this elaboration by performing expert interviews with leaders. In total seventeen companies could be questioned. The results indicate that AI is not widely used in leadership yet since only one company uses it currently and just about 10% of the participants plan the implementation in the closer feature. While the following items ex- plain why companies want to use AI in leadership: Chances for automation, time and cost savings, many important disadvantages and issues prevent companies from actively using it now: No areas of application are known, no need justifies the use, human interactions as a key aspect of leadership is reduced and it is hard to collect all necessary data. Beyond that, it was aimed to identify changes in the field of leadership through the use of AI. This objective could not be addressed due to the limited number of participants using AI in leadership.
Keywords: Leadership, artificial intelligence, transformation, state-of-use
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.
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.
The novel mobile application csxPOI (short for: collaborative, semantic, and context-aware points-of-interest) enables its users to collaboratively create, share, and modify semantic points of interest (POI). Semantic POIs describe geographic places with explicit semantic properties of a collaboratively created ontology. As the ontology includes multiple subclassiffcations and instantiations and as it links to DBpedia, the richness of annotation goes far beyond mere textual annotations such as tags. With the intuitive interface of csxPOI, users can easily create, delete, and modify their POIs and those shared by others. Thereby, the users adapt the structure of the ontology underlying the semantic annotations of the POIs. Data mining techniques are employed to cluster and thus improve the quality of the collaboratively created POIs. The semantic POIs and collaborative POI ontology are published as Linked Open Data.
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.
With the Multimedia Metadata Ontology (M3O), we have developed a sophisticated model for representing among others the annotation, decomposition, and provenance of multimedia metadata. The goal of the M3O is to integrate the existing metadata standards and metadata formats rather than replacing them. To this end, the M3O provides a scaffold needed to represent multimedia metadata. Being an abstract model for multimedia metadata, it is not straightforward how to use and specialize the M3O for concrete application requirements and existing metadata formats and metadata standards. In this paper, we present a step-by-step alignment method describing how to integrate and leverage existing multimedia metadata standards and metadata formats in the M3O in order to use them in a concrete application. We demonstrate our approach by integrating three existing metadata models: the Core Ontology on Multimedia (COMM), which is a formalization of the multimedia metadata standard MPEG-7, the Ontology for Media Resource of the W3C, and the widely known industry standard EXIF for image metadata
Expert-driven business process management is an established means for improving efficiency of organizational knowledge work. Implicit procedural knowledge in the organization is made explicit by defining processes. This approach is not applicable to individual knowledge work due to its high complexity and variability. However, without explicitly described processes there is no analysis and efficient communication of best practices of individual knowledge work within the organization. In addition, the activities of the individual knowledge work cannot be synchronized with the activities in the organizational knowledge work.rnrnSolution to this problem is the semantic integration of individual knowledgernwork and organizational knowledge work by means of the patternbased core ontology strukt. The ontology allows for defining and managing the dynamic tasks of individual knowledge work in a formal way and to synchronize them with organizational business processes. Using the strukt ontology, we have implemented a prototype application for knowledge workers and have evaluated it at the use case of an architectural fifirm conducting construction projects.
Das Interesse am Konzept Crowdfunding ist in den letzten Jahren sowohl aus der Wirtschaft als auch aus der Wissenschaft gestiegen. Neben Künstlern und Entrepreneuren finanzieren nun auch Wissenschaftler ihre Projekte durch zahlreiche kleine Beiträge aus der Crowd. Allerdings spiegelt die wahrgenommene Nutzung in Deutschland nicht die Vorteile einer Crowdfunding-Kampagne wider, insbesondere nicht im internationalen Vergleich. Die vorliegende Studie untersucht diesen Umstand, indem sie die Motive und Barrieren für eine Finanzierung durch Crowdfunding identifiziert, um Empfehlungen für Forschungseinrichtungen zur Förderung von Crowdfunding zu formulieren. Durch eine Literaturanalyse werden erste Erkenntnisse ermittelt, welche dann für die Durchführung von qualitativen Interviews mit elf Wissenschaftlern, die bereits eine Crowdfunding-Kampagne erfolgreich abgeschlossen haben, verwendet werden. Die Ergebnisse zeigen, dass ForscherInnen in Deutschland Crowdfunding in erster Linie dazu verwenden, Aufmerksamkeit für das Thema und die wissenschaftliche Gemeinschaft im Allgemeinen zu schaffen. Die größten Barrieren sind der enorme Aufwand, der mit einer Kampagne verbunden ist, und die mangelnde Reputation des Konzepts des Crowdfunding seitens der deutschen Wissenschaft. Zudem eignen sich nur Themen und Projekte mit einer hohen Öffentlichkeitswirksamkeit und einem Fördervolumen von maximal fünfstelligen Beträgen. Darüber hinaus konnte die öffentliche Wahrnehmung der Experten während der Kampagne als zusätzliche Barriere identifiziert werden.
Diese Ergebnisse führen zu drei Empfehlungen für Forschungseinrichtungen zur Förderung von Crowdfunding: Es wird empfohlen das Bewusstsein für das Thema Crowdfunding als zusätzliche Form der Forschungsfinanzierung zu sensibilisieren und die Vorteile einer Crowdfunding-Kampagne hervorzuheben. Universitäten sollten mit Crowdfunding Akteuren (bspw. Plattformen und Experten) zusammenarbeiten und die Netzwerkeffekte einer Universität sollten genutzt werden. Die Universitäten sollten Unterstützung leisten, um die Arbeitsbelastung auf interdisziplinäre Teams zu verteilen, um so das Verhältnis zwischen Aufwand und Ertrag zu optimieren. Die gewählte Methodik und der Geltungsbereich der Thesis eröffnen weitere Forschungsmöglichkeiten, die die Perspektive der Universitäten und die Bedingungen in anderen Ländern untersuchen könnten. Darüber hinaus ist eine groß angelegte quantitative Studie erforderlich, um die identifizierten Konzepte statistisch zu validieren.
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.
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.
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.