## Fachbereich Informatik

### Refine

#### Year of publication

#### Document Type

- Article (92) (remove)

#### Language

- English (92) (remove)

#### Keywords

- AG-RESY (32)
- PARO (24)
- SKALP (14)
- HANDFLEX (6)
- motion planning (5)
- industrial robots (4)
- parallel processing (4)
- LOADBAL (3)
- search algorithms (3)
- Case-Based Reasoning (2)

Background: The use of health apps to support the treatment of chronic pain is gaining importance. Most available pain management apps are still lacking in content quality and quantity as their developers neither involve health experts to ensure target group suitability nor use gamification to engage and motivate the user. To close this gap, we aimed to develop a gamified pain management app, Pain-Mentor.
Objective: To determine whether medical professionals would approve of Pain-Mentor’s concept and content, this study aimed to evaluate the quality of the app’s first prototype with experts from the field of chronic pain management and to discover necessary improvements.
Methods: A total of 11 health professionals with a background in chronic pain treatment and 2 mobile health experts participated in this study. Each expert first received a detailed presentation of the app. Afterward, they tested Pain-Mentor and then rated its quality using the mobile application rating scale (MARS) in a semistructured interview.
Results: The experts found the app to be of excellent general (mean 4.54, SD 0.55) and subjective quality (mean 4.57, SD 0.43). The app-specific section was rated as good (mean 4.38, SD 0.75). Overall, the experts approved of the app’s content, namely, pain and stress management techniques, behavior change techniques, and gamification. They believed that the use of gamification in Pain-Mentor positively influences the patients’ motivation and engagement and thus has the potential to promote the learning of pain management techniques. Moreover, applying the MARS in a semistructured interview provided in-depth insight into the ratings and concrete suggestions for improvement.
Conclusions: The experts rated Pain-Mentor to be of excellent quality. It can be concluded that experts perceived the use of gamification in this pain management app in a positive manner. This showed that combining pain management with gamification did not negatively affect the app’s integrity. This study was therefore a promising first step in the development of Pain-Mentor.

In this paper we present the results of the project “#Datenspende” where during the German election in 2017 more than 4000 people contributed their search results regarding keywords connected to the German election campaign.
Analyzing the donated result lists we prove, that the room for personalization of the search results is very small. Thus the opportunity for the effect mentioned in Eli Pariser’s filter bubble theory to occur in this data is also very small, to a degree that it is negligible. We achieved these results by applying various similarity measures to the result lists that were donated. The first approach using the number of common results as a similarity measure showed that the space for personalization is less than two results out of ten on average when searching for persons and at most four regarding the search for parties. Application of other, more specific measures show that the space is indeed smaller, so that the presence of filter bubbles is not evident.
Moreover this project is also a proof of concept, as it enables society to permanently monitor a search engine’s degree of personalization for any desired search terms. The general design can also be transferred to intermediaries, if appropriate APIs restrict selective access to contents relevant to the study in order to establish a similar degree of trustworthiness.

Patients after total hip arthroplasty (THA) suffer from lingering musculoskeletal restrictions. Three-dimensional (3D) gait analysis in combination with machine-learning approaches is used to detect these impairments. In this work, features from the 3D gait kinematics, spatio temporal parameters (Set 1) and joint angles (Set 2), of an inertial sensor (IMU) system are proposed as an input for a support vector machine (SVM) model, to differentiate impaired and non-impaired gait. The features were divided into two subsets. The IMU-based features were validated against an optical motion capture (OMC) system by means of 20 patients after THA and a healthy control group of 24 subjects. Then the SVM model was trained on both subsets. The validation of the IMU system-based kinematic features revealed root mean squared errors in the joint kinematics from 0.24° to 1.25°. The validity of the spatio-temporal gait parameters (STP) revealed a similarly high accuracy. The SVM models based on IMU data showed an accuracy of 87.2% (Set 1) and 97.0% (Set 2). The current work presents valid IMU-based features, employed in an SVM model for the classification of the gait of patients after THA and a healthy control. The study reveals that the features of Set 2 are more significant concerning the classification problem. The present IMU system proves its potential to provide accurate features for the incorporation in a mobile gait-feedback system for patients after THA.

3D joint kinematics can provide important information about the quality of movements. Optical motion capture systems (OMC) are considered the gold standard in motion analysis. However, in recent years, inertial measurement units (IMU) have become a promising alternative. The aim of this study was to validate IMU-based 3D joint kinematics of the lower extremities during different movements. Twenty-eight healthy subjects participated in this study. They performed bilateral squats (SQ), single-leg squats (SLS) and countermovement jumps (CMJ). The IMU kinematics was calculated using a recently-described sensor-fusion algorithm. A marker based OMC system served as a reference. Only the technical error based on algorithm performance was considered, incorporating OMC data for the calibration, initialization, and a biomechanical model. To evaluate the validity of IMU-based 3D joint kinematics, root mean squared error (RMSE), range of motion error (ROME), Bland-Altman (BA) analysis as well as the coefficient of multiple correlation (CMC) were calculated. The evaluation was twofold. First, the IMU data was compared to OMC data based on marker clusters; and, second based on skin markers attached to anatomical landmarks. The first evaluation revealed means for RMSE and ROME for all joints and tasks below 3°. The more dynamic task, CMJ, revealed error measures approximately 1° higher than the remaining tasks. Mean CMC values ranged from 0.77 to 1 over all joint angles and all tasks. The second evaluation showed an increase in the RMSE of 2.28°– 2.58° on average for all joints and tasks. Hip flexion revealed the highest average RMSE in all tasks (4.87°– 8.27°). The present study revealed a valid IMU-based approach for the measurement of 3D joint kinematics in functional movements of varying demands. The high validity of the results encourages further development and the extension of the present approach into clinical settings.

IoT systems consist of Hardware/Software systems (e.g., sensors) that are embedded in a physical world, networked and that interact with complex software platforms. The validation of such systems is a challenge and currently mostly done by prototypes. This paper presents the virtual environment for simulation, emulation and validation of an IoT platform and its semantic model in real life scenarios. It is based on a decentralized, bottom up approach that offers interoperability of IoT devices and the value-added services they want to use across different domains. The framework is demonstrated by a comprehensive case study. The example consists of the complete IoT “Smart Energy” use case with focus on data privacy by homomorphic encryption. The performance of the network is compared while using partially homomorphic encryption, fully homomorphic encryption and no encryption at all.As a major result, we found that our framework is capable of simulating big IoT networks and the overhead introduced by homomorphic encryption is feasible for VICINITY.

Postmortem Analysis of Decayed Online Social Communities: Cascade Pattern Analysis and Prediction
(2018)

Recently, many online social networks, such as MySpace, Orkut, and Friendster, have faced inactivity decay of their members, which contributed to the collapse of these networks. The reasons, mechanics, and prevention mechanisms of such inactivity decay are not fully understood. In this work, we analyze decayed and alive subwebsites from the Stack Exchange platform. The analysis mainly focuses on the inactivity cascades that occur among the members of these communities. We provide measures to understand the decay process and statistical analysis to extract the patterns that accompany the inactivity decay. Additionally, we predict cascade size and cascade virality using machine learning. The results of this work include a statistically significant difference of the decay patterns between the decayed and the alive subwebsites. These patterns are mainly cascade size, cascade virality, cascade duration, and cascade similarity. Additionally, the contributed prediction framework showed satisfactorily prediction results compared to a baseline predictor. Supported by empirical evidence, the main findings of this work are (1) there are significantly different decay patterns in the alive and the decayed subwebsites of the Stack Exchange; (2) the cascade’s node degrees contribute more to the decay process than the cascade’s virality, which indicates that the expert members of the Stack Exchange subwebsites were mainly responsible for the activity or inactivity of the Stack Exchange subwebsites; (3) the Statistics subwebsite is going through decay dynamics that may lead to it becoming fully-decayed; (4) the decay process is not governed by only one network measure, it is better described using multiple measures; (5) decayed subwebsites were originally less resilient to inactivity decay, unlike the alive subwebsites; and (6) network’s structure in the early stages of its evolution dictates the activity/inactivity characteristics of the network.

Self-adaptation allows software systems to autonomously adjust their behavior during run-time by handling all possible
operating states that violate the requirements of the managed system. This requires an adaptation engine that receives adaptation
requests during the monitoring process of the managed system and responds with an automated and appropriate adaptation
response. During the last decade, several engineering methods have been introduced to enable self-adaptation in software systems.
However, these methods lack addressing (1) run-time uncertainty that hinders the adaptation process and (2) the performance
impacts resulted from the complexity and the large number of the adaptation space. This paper presents CRATER, a framework
that builds an external adaptation engine for self-adaptive software systems. The adaptation engine, which is built on Case-based
Reasoning, handles the aforementioned challenges together. This paper is braced with an experiment illustrating the benefits of
this framework. The experimental results shows the potential of CRATER in terms handling run-time uncertainty and adaptation
remembrance that enhances the performance for large number of adaptation space.

In recent years, more and more publications and material for studying and teaching, e. g. for Web-based teaching (WBT), appear "online" and digital libraries are built to manage such publications and online materials. Therefore, the most important concerns are related to the problem of durable, sustained storage and the management of content together with its metadata existing in heterogeneous styles and formats. In this paper, we present specific techniques and their use to support metadata-based catalog services. Such semistructured metadata (represented as XML fragments), which belong to online learning resources, need efficient XML-based query support, scalable result set processing, and comprehensive facilities for personalization purposes. We discuss the associated problems, subsequently derive the concepts of a suitable architecture, and finally outline the realization by means of our prototype system that is based on the J2EE component model.

In many robotic applications, the teaching of points in space is necessary to register the robot coordinate system with the one of the application. Robot-human interaction is awkward and dangerous for the human because of the possibly large size and power of the robot, so robot movements must be predictable and natural. We present a novel hybrid control algorithm which provides the needed precision in small scale movements while allowing for fast and intuitive large scale translations.

It is difficult for robots to handle a vibrating deformable object. Even for human beings it is a high-risk operation to, for example, insert a vibrating linear object into a small hole. However, fast manipulation using a robot arm is not just a dream; it may be achieved if some important features of the vibration are detected online. In this paper, we present an approach for fast manipulation using a force/torque sensor mounted on the robot's wrist. Template matching method is employed to recognize the vibrational phase of the deformable objects. Therefore, a fast manipulation can be performed with a high success rate, even if there is acute vibration. Experiments inserting a deformable object into a hole are conducted to test the presented method. Results demonstrate that the presented sensor-based online fast manipulation is feasible.

Virtual Robot Programming for Deformable Linear Objects: System concept and Prototype Implementation
(2002)

In this paper we present a method and system for robot programming using virtual reality techniques. The proposed method allows intuitive teaching of a manipulation task with haptic feedback in a graphical simulation system. Based on earlier work, our system allows even an operator who lacks specialized knowledge of robotics to automatically generate a robust sensor-based robot program that is ready to execute on different robots, merely by demonstrating the task in virtual reality.

This paper analyzes the problem of sensor-based colli-sion detection for an industrial robotic manipulator. A method to perform collision tests based on images taken from several stationary cameras in the work cell is pre-sented. The collision test works entirely based on the im-ages, and does not construct a representation of the Carte-sian space. It is shown how to perform a collision test for all possible robot configurations using only a single set of images taken simultaneously.

We present a system concept allowing humans to work safely in the same environment as a robot manipulator. Several cameras survey the common workspace. A look-up-table-based fusion algorithm is used to back-project directly from the image spaces of the cameras to the manipulator?s con-figuration space. In the look-up-tables both, the camera calibration and the robot geometry are implicitly encoded. For experiments, a conven-tional 6 axis industrial manipulator is used. The work space is surveyed by four grayscale cameras. Due to the limits of present robot controllers, the computationally expensive parts of the system are executed on a server PC that communicates with the robot controller via Ethernet.

This paper deals with the handling of deformable linear objects (DLOs), such as hoses, wires or leaf springs. It investigates the a priori knowledge about the 6-dimensional force/torque signal for a changing contact situation between a DLO and a rigid polyhedral obstacle. The result is a complete list, containing for each contact change the most significant combination of force/torque signal components together with a description of the expected signal curve. This knowledge enables the reliable detection of changes in the DLO contact situation and with it the implementation of sensor-based manipulation skills for all possible contact changes.

Comprehensive reuse and systematic evolution of reuse artifacts as proposed by the Quality Improvement Paradigm (QIP) do not only require tool support for mere storage and retrieval. Rather, an integrated management of (potentially reusable) experience data as well as project-related data is needed. This paper presents an approach exploiting object-relational database technology to implement QIP-driven reuse repositories. Requirements, concepts, and implementational aspects are discussed and illustrated through a running example, namely the reuse and continuous improvement of SDL patterns for developing distributed systems. Our system is designed to support all phases of a reuse process and the accompanying improvement cycle by providing adequate functionality. Its implementation is based on object-relational database technology along with an infrastructure well suited for these purposes.

Software development organizations are recognizing the increasing importance of investing in the build-up of core competencies for their competitiveness in software system development. This is supported by reuse and experience repository systems that assist in capturing and reusing all kinds of software artifacts (e. g., code, patterns, frameworks) and processes as well as experiences related to these artifacts and processes. To justify such an investment and guide its improvement, it must be evaluated according to the business case, that is, a measurement program has to be developed that is oriented towards the business goals of such a reuse and experience repository system. In this paper, we suggest an approach to iteratively build up measurement programs for gaining feedback and, thereby, controlling and improving such a reuse and experience repository system. The focus is placed on guidelines for the evolution of such measurement programs over time, rather than providing directly applicable metrics or questionnaires. In order to illustrate the feasibility of the approach, examples of running measurement programs at different stages of evolutions are given.

For transferring existing knowledge into new projects, reuse has become an important factor in today's software industry. However, to set reuse into practice, reusable artifacts have to be stored somewhere, and must be offered to (re-)users on demand. For this purpose, advanced reuse repository systems like, for instance, instantiations of the Experience Base concept, are quite frequently used. Many people, from different projects, have to access such a repository at various phases of software development processes to retrieve or store reusable data. In order to fulfill the given tasks, each of these user has specific needs. Taking this into account, a reuse repository has to offer tailored user interfaces and functions for different user groups. Furthermore, since the contents of such a repository usually represent the state of the art of an organization's (core) competencies, not everyone should be allowed to freely access each and every repository entry. This isespecially true for persons that are not part of the organization. This report discusses role concepts that can be applied to reuse repository systems to overcome some of the stated access problems. Commonly used roles for software development and reuse repository management are listed. Based on these roles, a basic set of roles, as implemented in the SFB 501 Experience Base, is introduced.

We present two techniques for reasoning from cases to solve classification tasks: Induction and case-based reasoning. We contrast the two technologies (that are often confused) and show how they complement each other. Based on this, we describe how they are integrated in one single platform for reasoning from cases: The Inreca system.

The hallmark of traditional Artificial Intelligence (AI) research is the symbolic representation and processing of knowledge. This is in sharp contrast to many forms of human reasoning, which to an extraordinary extent, rely on cases and (typical) examples. Although these examples could themselves be encoded into logic, this raises the problem of restricting the corresponding model classes to include only the intended models.There are, however, more compelling reasons to argue for a hybrid representa-tion based on assertions as well as examples. The problems of adequacy, availability of information, compactness of representation, processing complexity, and last but not least, results from the psychology of human reasoning, all point to the same conclusion: Common sense reasoning requires different knowledge sources and hybrid reasoning principles that combine symbolic as well as semantic-based inference. In this paper we address the problem of integrating semantic representations of examples into automateddeduction systems. The main contribution is a formal framework for combining sentential with direct representations. The framework consists of a hybrid knowledge base, made up of logical formulae on the one hand and direct representations of examples on the other, and of a hybrid reasoning method based on the resolution calculus. The resulting hybrid resolution calculus is shown to be sound and complete.

Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading
(1999)

We develop an order-sorted higher-order calculus suitable forautomatic theorem proving applications by extending the extensional simplytyped lambda calculus with a higher-order ordered sort concept and constantoverloading. Huet's well-known techniques for unifying simply typed lambdaterms are generalized to arrive at a complete transformation-based unificationalgorithm for this sorted calculus. Consideration of an order-sorted logicwith functional base sorts and arbitrary term declarations was originallyproposed by the second author in a 1991 paper; we give here a correctedcalculus which supports constant rather than arbitrary term declarations, aswell as a corrected unification algorithm, and prove in this setting resultscorresponding to those claimed there.

An important research problem is the incorporation of "declarative" knowledge into an automated theorem prover that can be utilized in the search for a proof. An interesting pro-posal in this direction is Alan Bundy's approach of using explicit proof plans that encapsulatethe general form of a proof and is instantiated into a particular proof for the case at hand. Wegive some examples that show how a "declarative" highlevel description of a proof can be usedto find proofs of apparently "similiar" theorems by analogy. This "analogical" information isused to select the appropriate axioms from the database so that the theorem can be proved.This information is also used to adjust some options of a resolution theorem prover. In orderto get a powerful tool it is necessary to develop an epistemologically appropriate language todescribe proofs, for which a large set of examples should be used as a testbed. We presentsome ideas in this direction.

In this paper we are interested in using a firstorder theorem prover to prove theorems thatare formulated in some higher order logic. Tothis end we present translations of higher or-der logics into first order logic with flat sortsand equality and give a sufficient criterion forthe soundness of these translations. In addi-tion translations are introduced that are soundand complete with respect to L. Henkin's gen-eral model semantics. Our higher order logicsare based on a restricted type structure in thesense of A. Church, they have typed functionsymbols and predicate symbols, but no sorts.

In this article we formally describe a declarative approach for encoding plan operatorsin proof planning, the so-called methods. The notion of method evolves from the much studiedconcept tactic and was first used by Bundy. While significant deductive power has been achievedwith the planning approach towards automated deduction, the procedural character of the tacticpart of methods, however, hinders mechanical modification. Although the strength of a proofplanning system largely depends on powerful general procedures which solve a large class ofproblems, mechanical or even automated modification of methods is nevertheless necessary forat least two reasons. Firstly methods designed for a specific type of problem will never begeneral enough. For instance, it is very difficult to encode a general method which solves allproblems a human mathematician might intuitively consider as a case of homomorphy. Secondlythe cognitive ability of adapting existing methods to suit novel situations is a fundamentalpart of human mathematical competence. We believe it is extremely valuable to accountcomputationally for this kind of reasoning.The main part of this article is devoted to a declarative language for encoding methods,composed of a tactic and a specification. The major feature of our approach is that the tacticpart of a method is split into a declarative and a procedural part in order to enable a tractableadaption of methods. The applicability of a method in a planning situation is formulatedin the specification, essentially consisting of an object level formula schema and a meta-levelformula of a declarative constraint language. After setting up our general framework, wemainly concentrate on this constraint language. Furthermore we illustrate how our methodscan be used in a Strips-like planning framework. Finally we briefly illustrate the mechanicalmodification of declaratively encoded methods by so-called meta-methods.

Several activities around the world aim at integrating object-oriented data models with relational ones in order to improve database management systems. As a first result of these activities, object-relational database management systems (ORDBMS) are already commercially available and, simultaneously, are subject to several research projects. This (position) paper reports on our activities in exploiting object-relational database technology for establishing repository manager functionality supporting software engineering (SE) processes. We argue that some of the key features of ORDBMS can directly be exploited to fulfill many of the needs of SE processes. Thus, ORDBMS, as we think, are much better suited to support SE applications than any others. Nevertheless, additional functionality, e. g., providing adequate version management, is required in order to gain a completely satisfying SE repository. In order to remain flexible, we have developed a generative approach for providing this additional functionality. It remains to be seen whether this approach, in turn, can effectively exploit ORDBMS features. This paper, therefore, wants to show that ORDBMS can substantially contribute to both establishing and running SE repositories.

A straightforward formulation of a mathematical problem is mostly not ad-equate for resolution theorem proving. We present a method to optimize suchformulations by exploiting the variability of first-order logic. The optimizingtransformation is described as logic morphisms, whose operationalizations aretactics. The different behaviour of a resolution theorem prover for the sourceand target formulations is demonstrated by several examples. It is shown howtactical and resolution-style theorem proving can be combined.

We show how to buildup mathematical knowledge bases usingframes. We distinguish three differenttypes of knowledge: axioms, definitions(for introducing concepts like "set" or"group") and theorems (for relating theconcepts). The consistency of such know-ledge bases cannot be proved in gen-eral, but we can restrict the possibilit-ies where inconsistencies may be impor-ted to very few cases, namely to the oc-currence of axioms. Definitions and the-orems should not lead to any inconsisten-cies because definitions form conservativeextensions and theorems are proved to beconsequences.

In most cases higher-order logic is based on the (gamma)-calculus in order to avoid the infinite set of so-called comprehension axioms. However, there is a price to be paid, namelyan undecidable unification algorithm. If we do not use the(gamma) - calculus, but translate higher-order expressions intofirst-order expressions by standard translation techniques, we haveto translate the infinite set of comprehension axioms, too. Ofcourse, in general this is not practicable. Therefore such anapproach requires some restrictions such as the choice of thenecessary axioms by a human user or the restriction to certainproblem classes. This paper will show how the infinite class ofcomprehension axioms can be represented by a finite subclass,so that an automatic translation of finite higher-order prob-lems into finite first-order problems is possible. This trans-lation is sound and complete with respect to a Henkin-stylegeneral model semantics.

Extending existing calculi by sorts is astrong means for improving the deductive power offirst-order theorem provers. Since many mathemat-ical facts can be more easily expressed in higher-orderlogic - aside the greater power of higher-order logicin principle - , it is desirable to transfer the advant-ages of sorts in the first-order case to the higher-ordercase. One possible method for automating higher-order logic is the translation of problem formulationsinto first-order logic and the usage of first-order the-orem provers. For a certain class of problems thismethod can compete with proving theorems directlyin higher-order logic as for instance with the TPStheorem prover of Peter Andrews or with the Nuprlproof development environment of Robert Constable.There are translations from unsorted higher-order lo-gic based on Church's simple theory of types intomany-sorted first-order logic, which are sound andcomplete with respect to a Henkin-style general mod-els semantics. In this paper we extend correspond-ing translations to translations of order-sorted higher-order logic into order-sorted first-order logic, thus weare able to utilize corresponding first-order theoremprover for proving higher-order theorems. We do notuse any (lambda)-expressions, therefore we have to add so-called comprehension axioms, which a priori makethe procedure well-suited only for essentially first-order theorems. However, in practical applicationsof mathematics many theorems are essentially first-order and as it seems to be the case, the comprehen-sion axioms can be mastered too.

Higher-Order Tableaux
(1999)

Even though higher-order calculi for automated theorem prov-ing are rather old, tableau calculi have not been investigated yet. Thispaper presents two free variable tableau calculi for higher-order logicthat use higher-order unification as the key inference procedure. Thesecalculi differ in the treatment of the substitutional properties of equival-ences. The first calculus is equivalent in deductive power to the machine-oriented higher-order refutation calculi known from the literature, whereasthe second is complete with respect to Henkin's general models.

Many mathematical proofs are hard to generate forhumans and even harder for automated theoremprovers. Classical techniques of automated theoremproving involve the application of basic rules, of built-in special procedures, or of tactics. Melis (Melis 1993)introduced a new method for analogical reasoning inautomated theorem proving. In this paper we showhow the derivational analogy replay method is relatedand extended to encompass analogy-driven proof planconstruction. The method is evaluated by showing theproof plan generation of the Pumping Lemma for con-text free languages derived by analogy with the proofplan of the Pumping Lemma for regular languages.This is an impressive evaluation test for the analogicalreasoning method applied to automated theorem prov-ing, as the automated proof of this Pumping Lemmais beyond the capabilities of any of the current auto-mated theorem provers.

This paper addresses the decomposition of proofs as a means of constructingmethods in plan-based automated theorem proving. It shows also, howdecomposition can beneficially be applied in theorem proving by analogy.Decomposition is also useful for human-style proof presentation. We proposeseveral decomposition techniques that were found to be useful in automatedtheorem proving and give examples of their application.

This paper analyzes how mathematicians prove the-orems. The analysis is based upon several empiricalsources such as reports of mathematicians and math-ematical proofs by analogy. In order to combine thestrength of traditional automated theorem provers withhuman-like capabilities, the questions arise: Whichproblem solving strategies are appropriate? Which rep-resentations have to be employed? As a result of ouranalysis, the following reasoning strategies are recog-nized: proof planning with partially instantiated meth-ods, structuring of proofs, the transfer of subproofs andof reformulated subproofs. We discuss the represent-ation of a component of these reasoning strategies, aswell as its properties. We find some mechanisms neededfor theorem proving by analogy, that are not providedby previous approaches to analogy. This leads us to acomputational representation of new components andprocedures for automated theorem proving systems.

As global networks are being used by more and more people,they are becoming increasingly interesting for commercial appli-cations. The recent success and change in direction of the World-Wide Web is a clear indication for this. However, this success meta largely unprepared communications infrastructure. The Inter-net as an originally non-profit network did neither offer the secu-rity, nor the globally available accounting infrastructure byitself.These problems were addressed in the recent past, but in aseemingly ad-hoc manner. Several different accounting schemessensible for only certain types of commercial transactions havebeen developed, which either seem to neglect the problems ofscalability, or trade security for efficiency. Finally, some propos-als aim at achieving near perfect security at the expense of effi-ciency, thus rendering those systems to be of no practical use.In contrast, this paper presents a suitably configurable schemefor accounting in a general, widely distributed client/server envi-ronment. When developing the protocol presented in this paper,special attention has been paid to make this approach work wellin the future setting of high-bandwidth, high-latency internets.The developed protocol has been applied to a large-scale distrib-uted application, a WWW-based software development environ-ment.

In this paper, we compare the BERKOM globally ac-cessible services project (GLASS) with the well-knownWorld-Wide Web with respect to the ease of development,realization, and distribution of multimedia presentations.This comparison is based on the experiences we gainedwhen implementing a gateway between GLASS and theWorld-Wide Web. Since both systems are shown to haveobvious weaknesses, we are concluding this paper with apresentation of a better way to multimedia document en-gineering and distribution. This concept is based on awell-accepted approach to function-shipping in the Inter-net: the Java language, permitting for example a smoothintegration of GLASS92 MHEG objects and WWW HTMLpages within one common environment.

In this paper, a framework for globally distributed soft-ware development and management environments, whichwe call Booster is presented. Additionally, the first experi-ences with WebMake, an application developed to serve asan experimental platform for a software developmentenvironment based on the World Wide Web and theBooster framework is introduced. Booster encompasses thebasic building blocks and mechanisms necessary tosupport a truly cooperative distributed softwaredevelopment from the very beginning to the last steps in asoftware life cycle. It is thus a precursor of the GlobalSoftware Highway, in which providers and users can meetfor the development, management, exchange and usage ofall kind of software.

In order to reduce the elapsed time of a computation, a pop-ular approach is to decompose the program into a collection of largelyindependent subtasks which are executed in parallel. Unfortunately, it isoften observed that tightly-coupled parallel programs run considerablyslower than initially expected. In this paper, a framework for the anal-ysis of parallel programs and their potential speedup is presented. Twoparameters which strongly affect the scalability of parallelism are iden-tified, namely the grain of synchronization, and the degree to which thetarget hardware is available. It is shown that for certain classes of appli-cations speedup is inherently poor, even if the program runs under theidealized conditions of perfect load balance, unbounded communicationbandwidth and negligible communication and parallelization overhead.Upper bounds are derived for the speedup that can be obtained in threedifferent types of computations. An example illustrates the main find-ings.

In this paper we generalize the notion of method for proofplanning. While we adopt the general structure of methods introducedby Alan Bundy, we make an essential advancement in that we strictlyseparate the declarative knowledge from the procedural knowledge. Thischange of paradigm not only leads to representations easier to under-stand, it also enables modeling the important activity of formulatingmeta-methods, that is, operators that adapt the declarative part of exist-ing methods to suit novel situations. Thus this change of representationleads to a considerably strengthened planning mechanism.After presenting our declarative approach towards methods we describethe basic proof planning process with these. Then we define the notion ofmeta-method, provide an overview of practical examples and illustratehow meta-methods can be integrated into the planning process.

Extending the planADbased paradigm for auto-mated theorem proving, we developed in previ-ous work a declarative approach towards rep-resenting methods in a proof planning frame-work to support their mechanical modification.This paper presents a detailed study of a classof particular methods, embodying variations ofa mathematical technique called diagonaliza-tion. The purpose of this paper is mainly two-fold. First we demonstrate that typical math-ematical methods can be represented in ourframework in a natural way. Second we illus-trate our philosophy of proof planning: besidesplanning with a fixed repertoire of methods,metaADmethods create new methods by modify-ing existing ones. With the help of three differ-ent diagonalization problems we present an ex-ample trace protocol of the evolution of meth-ods: an initial method is extracted from a par-ticular successful proof. This initial method isthen reformulated for the subsequent problems,and more general methods can be obtained byabstracting existing methods. Finally we comeup with a fairly abstract method capable ofdealing with all the three problems, since it cap-tures the very key idea of diagonalization.

Most automated theorem provers suffer from the problem thatthey can produce proofs only in formalisms difficult to understand even forexperienced mathematicians. Effort has been made to reconstruct naturaldeduction (ND) proofs from such machine generated proofs. Although thesingle steps in ND proofs are easy to understand, the entire proof is usuallyat a low level of abstraction, containing too many tedious steps. To obtainproofs similar to those found in mathematical textbooks, we propose a newformalism, called ND style proofs at the assertion level , where derivationsare mostly justified by the application of a definition or a theorem. Aftercharacterizing the structure of compound ND proof segments allowing asser-tion level justification, we show that the same derivations can be achieved bydomain-specific inference rules as well. Furthermore, these rules can be rep-resented compactly in a tree structure. Finally, we describe a system calledPROVERB , which substantially shortens ND proofs by abstracting them tothe assertion level and then transforms them into natural language.

Planning Argumentative Texts
(1999)

This paper presents PROVERB a text planner forargumentative texts. PROVERB's main feature isthat it combines global hierarchical planning and un-planned organization of text with respect to local de-rivation relations in a complementary way. The formersplits the task of presenting a particular proof intosubtasks of presenting subproofs. The latter simulateshow the next intermediate conclusion to be presentedis chosen under the guidance of the local focus.

This paper deals with the reference choices involved in thegeneration of argumentative text. A piece of argument-ative text such as the proof of a mathematical theoremconveys a sequence of derivations. For each step of de-rivation, the premises (previously conveyed intermediateresults) and the inference method (such as the applica-tion of a particular theorem or definition) must be madeclear. The appropriateness of these references cruciallyaffects the quality of the text produced.Although not restricted to nominal phrases, our refer-ence decisions are similar to those concerning nominalsubsequent referring expressions: they depend on theavailability of the object referred to within a context andare sensitive to its attentional hierarchy . In this paper,we show how the current context can be appropriatelysegmented into an attentional hierarchy by viewing textgeneration as a combination of planned and unplannedbehavior, and how the discourse theory of Reichmann canbe adapted to handle our special reference problem.

Most automated theorem provers suffer from the problemthat the resulting proofs are difficult to understand even for experiencedmathematicians. An effective communication between the system andits users, however, is crucial for many applications, such as in a mathematical assistant system. Therefore, efforts have been made to transformmachine generated proofs (e.g. resolution proofs) into natural deduction(ND) proofs. The state-of-the-art procedure of proof transformation fol-lows basically its completeness proof: the premises and the conclusionare decomposed into unit literals, then the theorem is derived by mul-tiple levels of proofs by contradiction. Indeterminism is introduced byheuristics that aim at the production of more elegant results. This inde-terministic character entails not only a complex search, but also leads tounpredictable results.In this paper we first study resolution proofs in terms of meaningful op-erations employed by human mathematicians, and thereby establish acorrespondence between resolution proofs and ND proofs at a more ab-stract level. Concretely, we show that if its unit initial clauses are CNFsof literal premises of a problem, a unit resolution corresponds directly toa well-structured ND proof segment that mathematicians intuitively un-derstand as the application of a definition or a theorem. The consequenceis twofold: First it enhances our intuitive understanding of resolutionproofs in terms of the vocabulary with which mathematicians talk aboutproofs. Second, the transformation process is now largely deterministicand therefore efficient. This determinism also guarantees the quality ofresulting proofs.

Even though it is not very often admitted, partial functionsdo play a significant role in many practical applications of deduction sys-tems. Kleene has already given a semantic account of partial functionsusing a three-valued logic decades ago, but there has not been a satisfact-ory mechanization. Recent years have seen a thorough investigation ofthe framework of many-valued truth-functional logics. However, strongKleene logic, where quantification is restricted and therefore not truth-functional, does not fit the framework directly. We solve this problemby applying recent methods from sorted logics. This paper presents atableau calculus that combines the proper treatment of partial functionswith the efficiency of sorted calculi.

The semantics of everyday language and the semanticsof its naive translation into classical first-order language consider-ably differ. An important discrepancy that is addressed in this paperis about the implicit assumption what exists. For instance, in thecase of universal quantification natural language uses restrictions andpresupposes that these restrictions are non-empty, while in classi-cal logic it is only assumed that the whole universe is non-empty.On the other hand, all constants mentioned in classical logic arepresupposed to exist, while it makes no problems to speak about hy-pothetical objects in everyday language. These problems have beendiscussed in philosophical logic and some adequate many-valuedlogics were developed to model these phenomena much better thanclassical first-order logic can do. An adequate calculus, however, hasnot yet been given. Recent years have seen a thorough investigationof the framework of many-valued truth-functional logics. UnfortuADnately, restricted quantifications are not truth-functional, hence theydo not fit the framework directly. We solve this problem by applyingrecent methods from sorted logics.

Typical instances, that is, instances that are representative for a particular situ-ation or concept, play an important role in human knowledge representationand reasoning, in particular in analogical reasoning. This wellADknown obser-vation has been a motivation for investigations in cognitive psychology whichprovide a basis for our characterization of typical instances within conceptstructures and for a new inference rule for justified analogical reasoning withtypical instances. In a nutshell this paper suggests to augment the proposi-tional knowledge representation system by a non-propositional part consistingof concept structures which may have directly represented instances as ele-ments. The traditional reasoning system is extended by a rule for justifiedanalogical inference with typical instances using information extracted fromboth knowledge representation subsystems.