AMS eBook CollectionsOne of the world's most respected mathematical collections, available in digital format for your library or institution
Automated Theorem Proving: After 25 Years
About this Title
W. W. Bledsoe and D. W. Loveland, Editors
Publication: Contemporary Mathematics
Publication Year:
1984; Volume 29
ISBNs: 978-0-8218-5027-5 (print); 978-0-8218-7614-5 (online)
DOI: https://doi.org/10.1090/conm/029
MathSciNet review: 749236
Table of Contents
Download chapters as PDF
Front/Back Matter
Articles
- Donald W. Loveland – Automated theorem-proving: a quarter-century review [MR 749237]
- Martin Davis, David Luckham and John McCarthy – Citation for Hao Wang as winner of the milestone award in automated theorem-proving [MR 749238]
- Hao Wang – Computer theorem proving and artificial intelligence [MR 749239]
- Nils J. Nilsson, Robert Boyer, Donald Loveland and R. Daniel Mauldin – Citation for Lawrence Wos and Steven Winker as Winners of the Current Research Award in Automated Theorem Proving
- L. Wos and S. Winker – Open Questions Solved with the Assistance of AURA
- W. W. Bledsoe – Some Automatic Proofs in Analysis
- Robert S Boyer and J Strother Moore – Proof-Checking, Theorem-Proving, and Program Verification
- Robert S Boyer and J Strother Moore – A Mechanical Proof of the Turing Completeness of Pure Lisp
- Peter B. Andrews, Dale A. Miller, Eve Longini Cohen and Frank Pfenning – Automating Higher-Order Logic
- D. Lankford, G. Butler and B. Brady – Abelian group unification algorithms for elementary terms [MR 749246]
- Greg Nelson – Combining Satisfiability Procedures by Equality-Sharing
- Wu Wen-Tsün – On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry
- Wu Wen-tsün – Some Recent Advances in Mechanical Theorem-Proving of Geometries
- Shang-Ching Chou – Proving Elementary Geometry Theorems Using Wu’s Algorithm
- Douglas B. Lenat – Automated Theory Formation in Mathematics
- James McDonald and Patrick Suppes – Student Use of an Interactive Theorem Prover