MARC 主機 00000cam  2200445Ma 4500 
001    774694026 
003    OCoLC 
005    20140507051322.0 
006    m     |||||||||||| 
007    cr c||---||||| 
008    840412s1984    riu     ob    100 0 eng d 
010    |z84009226 
020    9780821876145 (online) 
020    0821876147 (online) 
020    9780821853832 (google) 
020    082185383X (google) 
020    9780821850275 
020    082185027X (pbk.) 
035    (OCoLC)774694026 
050 14 QA76.9.A96|bS64 1983 
082 04 511.3|219 
111 2  Special Session on Automatic Theorem Proving|d(1983 :
       |cDenver, Colo.) 
245 10 Automated theorem proving|h[electronic resource]:|bafter 
       25 years /|cW.W. Bledsoe and D.W. Loveland, editors 
260    Providence, R.I. :|bAmerican Mathematical Society,|c1984 
300    1 online resource (ix, 360 p.) 
490 1  Contemporary mathematics,|x0271-4132 ;|vv. 29 
500    "Proceedings of the Special Session on Automatic Theorem 
       Proving, 89th Annual Meeting of the American Mathematical 
       Society, held in Denver, Colorado, January 5-9, 1983"--
       T.p. verso 
504    Includes bibliographies 
505 00 |tAutomated theorem-proving: a quarter-century review /
       |rDonald W. Loveland --|u
       |u|tCitation for 
       Hao Wang as winner of the milestone award in automated 
       theorem-proving /|rMartin Davis, David Luckham and John 
       McCarthy --|u|uhttp://|tComputer theorem 
       proving and artificial intelligence /|rHao Wang --|uhttp:/
       /749239|tCitation for Lawrence Wos and Steven Winker as 
       Winners of the Current Research Award in Automated Theorem
       Proving /|rNils J. Nilsson, Robert Boyer, Donald Loveland 
       and R. Daniel Mauldin --|u
       |u|tOpen Questions 
       Solved with the Assistance of AURA /|rL. Wos and S. Winker
       10.1090/conm/029/05|tSome Automatic Proofs in Analysis /
       |rW. W. Bledsoe --|u|uhttp://|tProof-Checking, Theorem-
       Proving, and Program Verification /|rRobert S Boyer and J 
       Strother Moore --|u|uhttp://|tA Mechanical Proof of the 
       Turing Completeness of Pure Lisp /|rRobert S Boyer and J 
       Strother Moore --|u|uhttp://|tAutomating Higher-Order 
       Logic /|rPeter B. Andrews, Dale A. Miller, Eve Longini 
       Cohen and Frank Pfenning --|u
       |u|tAbelian group 
       unification algorithms for elementary terms /|rD. Lankford,
       G. Butler and B. Brady --|u
       Satisfiability Procedures by Equality-Sharing /|rGreg 
       Nelson --|u|u
       /10.1090/conm/029/11|tOn the Decision Problem and the 
       Mechanization of Theorem-Proving in Elementary Geometry /
       |rWu Wen-Tsün --|u|uhttp://|tSome Recent Advances in 
       Mechanical Theorem-Proving of Geometries /|rWu Wen-tsün --
       conm/029/13|tProving Elementary Geometry Theorems Using 
       Wu's Algorithm /|rShang-Ching Chou --|u
       |tAutomated Theory Formation in Mathematics /|rDouglas B. 
       Lenat --|u|u
       10.1090/conm/029/15|tStudent Use of an Interactive Theorem
       Prover /|rJames McDonald and Patrick Suppes --|uhttp://|u
650  0 Automatic theorem proving|xCongresses 
650  7 Automatic theorem proving.|2fast|0(OCoLC)fst00822777 
655  7 Conference proceedings.|2fast|0(OCoLC)fst01423772 
700 1  Bledsoe, W. W 
700 1  Loveland, Donald W 
710 2  American Mathematical Society 
830  0 Contemporary mathematics (American Mathematical Society) ;
       |vv. 29 
856 4  |u