Table of contents

  1. Front Matter
  2. Pages 1-9
  3. Pages 11-31
  4. Pages 63-94
  5. Pages 95-107
  6. Pages 109-154
  7. Pages 183-205
  8. Back Matter

About this book


This monograph is the result of the cooperation of a mathematician working in universal algebra and geometry, and a computer scientist working in automated deduction, who succeeded in employing the theorem prover Otter for proving first order theorems from mathematics and then intensified their joint effort.
Mathematicians will find many new results from equational logic, universal algebra, and algebraic geometry and benefit from the state-of-the-art outline of the capabilities of automated deduction techniques. Computer scientists will find a large and varied source of theorems and problems that will be useful in designing and evaluation automated theorem proving systems and strategies.


Autoated Theorem Proving Automat Automatisches Schließen Automatisches Theorembeweisen Cubic Curves Equatgional Logic Equational Logik Kubische Kurven Universal Algebra Universelles Algebra automated deduction automated theorem proving logic proving theorem proving

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 1996
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Springer Book Archive
  • Print ISBN 978-3-540-61398-5
  • Online ISBN 978-3-540-68522-7
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
Materials & Steel
Chemical Manufacturing
Finance, Business & Banking
IT & Software
Consumer Packaged Goods
Energy, Utilities & Environment
Oil, Gas & Geosciences