© 1998

Automated Deduction — A Basis for Applications

Volume II: Systems and Implementation Techniques

  • Wolfgang Bibel
  • Peter H. Schmitt

Part of the Applied Logic Series book series (APLS, volume 9)

Table of contents

  1. Front Matter
    Pages i-xiv
  2. Interactive Theorem Proving

    1. Front Matter
      Pages 1-11
    2. W. Reif, G. Schellhorn, K. Stenzel, M. Balser
      Pages 13-39
    3. Benl, Berger, Schwichtenberg, Seisenberger, Zuber
      Pages 41-71
    4. M. Strecker, M. Luther, F. Von Henke
      Pages 73-96
    5. Ahrendt, Beckert, Hähnle, Menzel, Reif, Schellhorn et al.
      Pages 97-116
  3. Representation and Optimization Techniques

    1. Front Matter
      Pages 117-123
    2. P. Graf, D. Fehrer
      Pages 125-147
    3. Gerd Neugebauer, Uwe Petermann
      Pages 167-188
    4. Thomas Kolbe, Christoph Walther
      Pages 189-219
  4. Parallel Inference Systems

    1. Front Matter
      Pages 221-229
    2. Bündgen, Göbel, Küchlin, Weber
      Pages 231-259
    3. Johann Schumann, Andreas Wolf, Christian Suttner
      Pages 261-290
    4. Bornscheuer, Hölldobler, Kalinke, Strohmaier
      Pages 291-321
  5. Comparison and Cooperation of Theorem Provers

    1. Front Matter
      Pages 323-329
    2. M. Baaz, U. Egly, A. Leitsch
      Pages 331-359
    3. Jörg Denzinger, Matthias Fuchs
      Pages 361-382
    4. Jörg Denzinger, Ingo Dahn
      Pages 383-416
  6. Back Matter
    Pages 417-434

About this book


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.


Boolean algebra Processing automata automated deduction automated reasoning automated theorem proving complex system expert system heuristics interactive theorem proving logic logic programming natural language proving term rewriting

Editors and affiliations

  • Wolfgang Bibel
    • 1
  • Peter H. Schmitt
    • 2
  1. 1.Darmstadt University of TechnologyGermany
  2. 2.Institute for Logic, Complexity and Deduction SystemsUniversity of KarlsruheKarlsruheGermany

Bibliographic information