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

1. Front Matter

   Pages i-xii

   PDF

2. Automated theorem proving in Mathematics

   1. Front Matter

      Pages 1-7

      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

      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

   PDF

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.

• Evolution
• Extension
• automated reasoning
• automated theorem proving
• calculus
• complex system
• expert system
• formal method
• heuristics
• natural language
• optimization
• programming
• proving
• term rewriting
• verification

• Darmstadt University of Technology, Germany

  Wolfgang Bibel

• University of Karlsruhe, Germany

  Peter H. Schmitt

Policies and ethics