Bøger af Wolfgang Bibel

1. BASIC CONCEPTS OF INTERACTIVE THEOREM PROVING Interactive Theorem Proving ultimately aims at the construction of powerful reasoning tools that let us (computer scientists) prove things we cannot prove without the tools, and the tools cannot prove without us. Interaction typi- cally is needed, for example, to direct and control the reasoning, to speculate or generalize strategic lemmas, and sometimes simply because the conjec- ture to be proved does not hold. In software verification, for example, correct versions of specifications and programs typically are obtained only after a number of failed proof attempts and subsequent error corrections. Different interactive theorem provers may actually look quite different: They may support different logics (first-or higher-order, logics of programs, type theory etc.), may be generic or special-purpose tools, or may be tar- geted to different applications. Nevertheless, they share common concepts and paradigms (e.g. architectural design, tactics, tactical reasoning etc.). The aim of this chapter is to describe the common concepts, design principles, and basic requirements of interactive theorem provers, and to explore the band- width of variations. Having a 'person in the loop', strongly influences the design of the proof tool: proofs must remain comprehensible, - proof rules must be high-level and human-oriented, - persistent proof presentation and visualization becomes very important.

Die Gesellschaft fur Informatik (GI) zeichnet jedes Jahr eine Informatikdisser- tation durch einen Preis aus. Die Auswahl dieser Dissertation stutzt sich auf die von den Universitaten und Hochschulen fur diesen Preis vorgeschlagenen Dissertationen. Somit sind die Teilnehmer an dem Auswahlverfahren der GI bereits als "e;Preistrager"e; ihrer Hochschule ausgezeichnet. Der Ausschu der GI, der den Preistrager aus der Reihe der vorgeschlagenen Kandidaten nominiert, veranstaltete in Raumen der Akademie der Wissen- schaften und Literatur Mainzein Kolloquium, das den Kandidaten Gelegenheit bot, ihre Resultate im Kreis der Mitbewerber vorzustellen und zu verteidigen. Der Ausschu war von dem hohen Niveau der eingereichten Arbeiten und der Prasentation sehr positiv beeindruckt. Die Teilnehmer begruten die Veran- staltung des Kolloquiums sehr, nahmen an der Diskussion teil und schatzten die Moglichkeit, mit den Teilnehmern aus anderen Hochschulen ins Gesprach zu kommen. Zu dem Erfolg des Kolloquiums trug auch die grozugige Gast- freundschaft der Akademie bei, der hier dafur auch gedankt sei. Es fiel dem Ausschu schwer, unter den nach dem Kolloquium in die engere Wahl genommenen Kandidaten den Preistrager zu bestimmen. Die Publikation der hier prasentierten Kurzfassungen gleicht die Ungerechtigkeit der Auswahl eines Kandidaten unter mehreren ebenburtigen Kandidaten etwas aus.

Since both the coments and the structure of the book appeared to be successful, only minor changes were made. As the world today has become so complex that humans apparently fail to manage it properly with their intellectual gifts, the realization of this dream might be regarded even as something like a necessity.

Das Gebiet der Wissenspräsentation und Inferenz umfaßt einen zentralen Bereich der Intellektik, d.h. des Gebietes der Künstlichen Intelligenz und der Kognitionswissenschaft. Es behandelt einerseits die Fragen nach einer formalen Beschreibung von Wissen jeglicher Art, besonders unter dem Aspekt einer maschinellen Verarbeitung in modernen Computern. Andererseits versucht es, das Alltagsschließen des Menschen so zu formalisieren, daß logische Schlüsse auch von Maschinen ausgeführt werden könnten. Das Buch gibt eine ausführliche Einführung in dieses umfangreiche Gebiet. Dem Studenten dient es im Rahmen einer solchen Vorlesung oder zum Selbststudium als umfassende Unterlage, und der Praktiker zieht einen großen Gewinn aus der Lektüre dieses modernen Stoffes, der in dieser Breite bisher nicht verfügbar war. Darüber hinaus leistet das Buch einen wichtigen Beitrag zur Forschung dadurch, daß viele Ansätze auf diesem Gebiet in ihren inneren Bezügen in ihrer Bedeutung klarer erkennbar werden und so eine solide Basis für die zukünftige Forschungsarbeit geschaffen ist. Der Leser ist nach der Lektüre dieses Werkes in der Lage, sich mit Details der Wissenspräsentation und Inferenz auseinanderzusetzen.

Among the dreams of mankind is the one dealing with the mecha­ nization of human thought. As the world today has become so complex that humans apparently fail to manage it properly with their intellectual gifts, the realization of this dream might be regarded even as something like a necessity. On the other hand, the incredible advances in computer technology let it appear as a real possibility. Of course, it is not easy to say what sort of thing human thinking actually is, a theme which over the centuries occupied many thinkers, mainly philosophers. From a critical point of view most of their theories were of a speculative nature since their only way of testing was by Gedanken-experi­ ments. It is the computer which has opened here a wide range of new possibilities since with this tool we now can model real experiments and thus test such theories like physicists do in their field. About a quarter of a century ago, scientific activi­ ties of that sort were started under the label of artificial intelligence Today these activities establish a wide and prosperous field which the author, in lack of any better name, prefers to call intellectics. Without any doubt, the com­ puter programs developed in this field have tought us much about the nature of human thinking.

Die Essays behandeln privates Erfahrungswissen und wissenschaftliche Erkenntnisse zu den Themenbereichen Körper, Geist, Seele, zwischenmenschliche Beziehungen,gesellschaftliche, wirtschaftliche und politische Strukturen sowie Wissenschaft, Religionund Kunst.