We propose an approach to the problem of proof control for our new first-order inductive theorem prover QuodLibet that is characterized by a great deal of flexibility w.r.t. the forms of proof control the prover supports. The approach is based on so-called (proof) tactics, i.e. proof control routines written in a special proof control language named QML. QuodLibet provides a set of tactics (in addition to the elementary inference rules), which range from tactics for trivial simplification steps to tactics representing comprehensive inductive proof strategies. Moreover, QuodLibet allows new tactics that are written by the user in QML to be integrated into the system to dynamically extend its functionality.
Der Trend zu einer immer stärkeren Kopplung von Systemen bei gleichzeitiger Dezentralisierung durch Vernetzung hat dazu geführt, daß Computernutzern auf Wunsch enorme Datenmengen zur Verfügung stehen, die sich einer sinnvollen Bearbeitung durch den Nutzer allein völlig entziehen. Unterschiedliche Repräsentationsformalismen für Informationen, Mehrdeutigkeiten, Redundanz sowie eingeschränkte Verfügbarkeit sowohl von Informationen als auch von Rechenleistung machen konventionelle Suchverfahren unanwendbar. Stattdessen werden Suchverfahren und Programme benötigt, die sich intelligent an unterschiedliche Formalismen anpassen, ihre Handlungen ständig evaluieren und fähig sind, ihre Benutzer individuell zu unterstützen. Schlagwörter wie Knowbots, Search-Engines oder Data-Miningsind deshalb zur Zeit in aller Munde. Ein umfassendes Buch, das die hinter diesen und ähnlichen Schlagwörtern verborgenen Ideen und Konzepte präsentiert, existiert jedoch zur Zeit noch nicht. Dies war für uns die Motivation, das Thema "Intelligente Suche im Internet mit Lernenden Systemen" in einem Seminar zu behandeln. Wir haben damit ein Forschungsgebiet aufgegriffen, das sowohl für alle am LSA beteiligten Gruppen von Interesse ist, aber darüber hinaus aktuell von vielen Seiten aufmerksam beobachtet wird. Daher haben wir uns entschlossen, die Ausarbeitungen, die im Rahmen dieses Seminars von den TeilmehmerInnen erstellt wurden, durch den vorliegenden Bericht einer breiteren Öffentlichkeit zugänglich zu machen.
We present an overview of various learning techniques used in automated theorem provers. We characterize the main problems arising in this context and classify the solutions to these problems from published approaches. We analyze the suitability of several combinations of solutions for different approaches to theorem proving and place these combinations in a spectrum ranging from provers using very specialized learning approaches to optimally adapt to a small class of proof problems, to provers that learn more general kinds of knowledge, resulting in systems that are less efficient in special cases but show improved performance for a wide range of problems. Finally, we suggest combinations of solutions for various proof philosophies.
Although it is acknowledged that internal iterators are easier and safer to use than conventional external iterators, it is commonly assumed that they are not applicable in languages without builtin support for closures and that they are less flexible than external iterators. We present an iteration framework that uses objects to emulate closures, separates structure exploration and data consumption, and generalizes on folding, thereby invalidating both the above statements. Our proposed "transfold" scheme allows processing one or more data structures simultaneously without exposing structure representations and without writing explicit loops. We show that the use of two functional concepts (function parameterization and lazy evaluation) within an object-oriented language allows combining the safety and economic usage of internal iteration with the flexibility and client control of external iteration. Sample code is provided using the statically typed EIFFEL language.
As the properties of components have gradually become clearer, attention has started to turn to the architectural issues which govern their interaction and composition. In this paper we identify some of the major architectural questions affecting component-based software develop-ment and describe the predominant architectural dimensions. Of these, the most interesting is the "architecture hierarchy" which we believe is needed to address the "interface vicissitude" problem that arises whenever interaction refinement is explicitly documented within a component-based system. We present a solution to this problem based on the concept of stratified architectures and object metamorphosis Finally, we describe how these concepts may assist in increasing the tailorability of component-based frameworks.
The value of software inspection for uncovering defects early in the development lifecycle has been well documented. Of the various types of inspection methods published to date, experiments have shown perspective-based inspection to be one of the most effective, because of its enhanced coverage of the defect space. However, inspections in general, and perspective-based inspections in particular, have so far been applied predominantly in the context of conventional structured development methods, and then almost always to textual artifacts, such as requirements documents or code modules. Object oriented-models, particularly of the graphical form, have so far not been adequately addressed by inspection methods. This paper tackles this problem by first discussing the difficulties involved in tailoring the perspective-based inspection approach to object-oriented development methods and, second, by presenting a generalization of the approach which overcomes these limitations. The new version of the approach is illustrated in the context of UML-based object-oriented development.
The interation of particular slender bodies with low Reynolds-number flows is in the limit 'slenderness to 0' described by a linear Fredholm integral equation of the second kind. The integral operator of this equation has a denumerable set of polynomial eigenfunctions whose corresponding eigenvalues are non-positive and of logarithmic growth. A theorem similiar to a classical result of Plemelj-Privalov for integral operators with Cauchy kernels is proven. In contrast to Cauchy kernel operators, the integral operator maps no Hölder space into itself. A spectral analysis of the integral operator restricted to an appropriate class of analytic functions is performed. The spectral properties of this restricted integral operator suggest a collocation-like method to solve the integral equation numerically. For this numerical scheme, convergence is proven and several computations are presented.