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. University of 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 10)

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 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 169.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 (12 chapters)

  1. Front Matter

    Pages i-xii
    Download chapter PDF

  2. Automated theorem proving in Mathematics

    1. Front Matter

      Pages 1-7
      Download chapter PDF

    2. Lattice-Ordered Groups in Deduction

      • Ingo Dahn
      Pages 9-29

    3. Superposition Theorem Proving for Commutative Rings

      • Jürgen Stuber
      Pages 31-55

    4. How to Augment a Formal System with a Boolean Algebra Component

      • Hans Jürgen Ohlbach, Jana Köhler
      Pages 57-75

    5. Proof Planning: A Practical Approach to Mechanized Reasoning in Mathematics

      • Manfred Kerber
      Pages 77-95

  3. Automated Deduction in Software Engineering and Hardware Design

    1. Front Matter

      Pages 97-104
      Download chapter PDF

    2. Program Synthesis

      • Christoph Kreitz
      Pages 105-134

    3. Termination Analysis for Functional Programs

      • Jürgen Giesl, Christoph Walther, Jürgen Brauburger
      Pages 135-164

    4. The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV

      • Gerhard Schellhorn, Wolfgang Ahrendt
      Pages 165-194

    5. Using Automated Theorem Provers in Verification of Protocols

      • Ingo Dahn, Johann Schumann
      Pages 195-224

    6. Theorem Proving in Large Theories

      • Wolfgang Reif, Gerhard Schellhorn
      Pages 225-241

    7. Analyzing Rule Sets for the Calculation of Banking Fees by a Theorem Prover with Constraints

      • Frieder Stolzenburg, Bernd Thomas
      Pages 243-264

    8. Deduction-Based Software Component Retrieval

      • Bernd Fischer, Johann Schumann, Gregor Snelting
      Pages 265-292

    9. Rewrite Based Hardware Verification with Redux

      • Reinhard Bündgen
      Pages 293-316

  4. Back Matter

    Pages 317-335
    Download chapter PDF
Back to top

Keywords

About this book

We are invited to deal with mathematical activity in a sys­ tematic way [ ... ] one does expect and look for pleasant surprises in this requirement of a novel combination of psy­ chology, logic, mathematics and technology. Hao Wang, 1970, quoted from(Wang, 1970). The field of mathematics has been a key application area for automated theorem proving from the start, in fact the very first automatically found the­ orem was that the sum of two even numbers is even (Davis, 1983). The field of automated deduction has witnessed considerable progress and in the last decade, automated deduction methods have made their way into many areas of research and product development in computer science. For instance, deduction systems are increasingly used in software and hardware verification to ensure the correctness of computer hardware and computer programs with respect to a given specification. Logic programming, while still falling somewhat short of its expectations, is now widely used, deduc­ tive databases are well-developed and logic-based description and analysis of hard-and software is commonplace today.

Editors and Affiliations

  • Darmstadt University of Technology, Germany

    Wolfgang Bibel

  • University of Karlsruhe, Germany

    Peter H. Schmitt

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation