| 000 | 02270nmm a2200193Ia 4500 | ||
|---|---|---|---|
| 008 | 230306s9999||||xx |||||||||||||||||und|| | ||
| 020 | _a9780821876145 (online) | ||
| 245 | 0 |
_aAutomated theorem proving : _bafter 25 years |
|
| 260 |
_aProvidence, R.I. : _bAmerican Mathematical Society, _c1984 |
||
| 300 | _a1 online resource (ix, 360 p.) | ||
| 490 |
_aContemporary mathematics _vv. 29 _x10983627 |
||
| 500 | _aProceedings of the Special Session on Automatic Theorem Proving, 89th Annual Meeting of the American Mathematical Society, held in Denver, Colorado, January 59, 1983T.p. verso. | ||
| 504 | _aIncludes bibliographies. | ||
| 505 |
_tAutomated theoremproving: a quartercentury review ; Citation for Hao Wang as winner of the milestone award in automated theoremproving ; Computer theorem proving and artificial intelligence ; Citation for Lawrence Wos and Steven Winker as Winners of the Current Research Award in Automated Theorem Proving ; Open Questions Solved with the Assistance of AURA ; Some Automatic Proofs in Analysis ; ProofChecking, TheoremProving, and Program Verification ; A Mechanical Proof of the Turing Completeness of Pure Lisp ; Automating HigherOrder Logic ; Abelian group unification algorithms for elementary terms ; Combining Satisfiability Procedures by EqualitySharing ; On the Decision Problem and the Mechanization of TheoremProving in Elementary Geometry ; Some Recent Advances in Mechanical TheoremProving of Geometries ; Proving Elementary Geometry Theorems Using Wu's Algorithm ; Automated Theory Formation in Mathematics ; Student Use of an Interactive Theorem Prover _rDonald W Loveland ; Martin Davis David Luckham and John McCarthy ; Hao Wang ; Nils J Nilsson Robert Boyer Donald Loveland and R Daniel Mauldin ; L Wos and S Winker ; W W Bledsoe ; Robert S Boyer and J Strother Moore ; Robert S Boyer and J Strother Moore ; Peter B Andrews Dale A Miller Eve Longini Cohen and Frank Pfenning ; D Lankford G Butler and B Brady ; Greg Nelson ; Wu WenTsun ; Wu Wentsun ; ShangChing Chou ; Douglas B Lenat ; James McDonald and Patrick Suppes |
||
| 650 | _aAutomatic theorem proving | ||
| 700 | _aBledsoe W W | ||
| 700 | _aLoveland Donald W | ||
| 856 | _uhttp://www.ams.org/conm/029/ | ||
| 999 |
_c28440 _d28440 |
||