Skip to main content
SpringerLink
Log in

Automated Deduction - A Basis for Applications Volume I Foundations - Calculi and Methods Volume II Systems and Implementation Techniques Volume III Applications

  • Book
  • © 1998

Overview

Editors:
  1. Wolfgang Bibel

    1. Darmstadt University of Technology, Germany

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Peter H. Schmitt

    1. Institute for Logic, Complexity and Deduction Systems, University of Karlsruhe, Karlsruhe, Germany

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (14 chapters)

  1. Front Matter

    Pages i-xiv
    Download chapter PDF

  2. Interactive Theorem Proving

    1. Front Matter

      Pages 1-11
      Download chapter PDF

    2. Structured Specifications and Interactive Proofs with KIV

      • W. Reif, G. Schellhorn, K. Stenzel, M. Balser
      Pages 13-39

    3. Proof Theory at Work: Program Development in the Minlog System

      • Benl, Berger, Schwichtenberg, Seisenberger, Zuber
      Pages 41-71

    4. Interactive and Automated Proof Construction in Type Theory

      • M. Strecker, M. Luther, F. Von Henke
      Pages 73-96

    5. Integrating Automated and Interactive Theorem Proving

      • Ahrendt, Beckert, Hähnle, Menzel, Reif, Schellhorn et al.
      Pages 97-116

  3. Representation and Optimization Techniques

    1. Front Matter

      Pages 117-123
      Download chapter PDF

    2. Term Indexing

      • P. Graf, D. Fehrer
      Pages 125-147

    3. Developing Deduction Systems: The Toolbox Style

      • D. Fehrer
      Pages 149-166

    4. Specifications of Inference Rules: Extensions of the PTTP Technique

      • Gerd Neugebauer, Uwe Petermann
      Pages 167-188

    5. Proof Analysis, Generalization and Reuse

      • Thomas Kolbe, Christoph Walther
      Pages 189-219

  4. Parallel Inference Systems

    1. Front Matter

      Pages 221-229
      Download chapter PDF

    2. Parallel Term Rewriting with Paredux

      • Bündgen, Göbel, Küchlin, Weber
      Pages 231-259

    3. Parallel Theorem Provers Based on Setheo

      • Johann Schumann, Andreas Wolf, Christian Suttner
      Pages 261-290

    4. Massively Parallel Reasoning

      • Bornscheuer, Hölldobler, Kalinke, Strohmaier
      Pages 291-321

  5. Comparison and Cooperation of Theorem Provers

    1. Front Matter

      Pages 323-329
      Download chapter PDF

    2. Extension Methods in Automated Deduction

      • M. Baaz, U. Egly, A. Leitsch
      Pages 331-359

    3. A Comparison of Equality Reasoning Heuristics

      • Jörg Denzinger, Matthias Fuchs
      Pages 361-382

    4. Cooperating Theorem Provers

      • Jörg Denzinger, Ingo Dahn
      Pages 383-416

  6. Back Matter

    Pages 417-434
    Download chapter PDF
Back to top

Keywords

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.

Editors and Affiliations

  • Darmstadt University of Technology, Germany

    Wolfgang Bibel

  • Institute for Logic, Complexity and Deduction Systems, University of Karlsruhe, Karlsruhe, Germany

    Peter H. Schmitt

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation