机读格式显示(MARC)

• 000 01839nam2 2200505 4500

• 000 1000008059

• 001 0000164348

• 003 CAL

• 005 20050126141834.0

• 008 900718s1990 gw a b 101 0 eng

• 010 __ |a 90010125

• 010 __ |a 90010125

• 020 __ |a 3540528857 |c CNY39.20

• 020 __ |a 0387528857 (U.S.)

• 040 __ |a DLC |c DLC |d DLC |a XAIT

• 050 00 |a QA76.9.A96 |b I57 1990

• 082 00 |a 511.3 |2 20

• 090 __ |a TP18-53/E21:10TH(90)

• 093 __ |a TP18-53 |2 4

• 099 __ |a CAL 022000222759 |a CAL 022001427435

• 111 2_ |a International Conference on Automated Deduction |n (10th : |d 1990 : |c Kaiserslautern, Germany)

• 245 10 |a 10th International Conference on Automated Deduction : |b proceedings : Kaiserslautern, FRG, July 24-27, 1990 / |c M.E. Stickel, (ed.).

• 246 30 |a Automated deduction

• 246 3_ |a Tenth International Conference on Automated Deduction

• 260 __ |a Berlin : |b Springer-Verlag, |c c1990.

• 300 __ |a xvi, 688 p. : |b ill. ; |c 24 cm.

• 440 _0 |a Lecture notes in computer science. |p Lecture notes in artificial intelligence ; |v 449

• 504 __ |a Includes biblioigraphical references and index.

• 650 _0 |a Logic, Symbolic and mathematical |v Congresses.

• 650 _0 |a Automatic theorem proving |v Congresses.

• 700 1_ |a Stickel, M. E. |q (Mark E.), |d 1947-

• 905 __ |a XATU |d TP18-53/E21:10TH(90)

• 920 __ |a 231030 |b O141-53 |c I61A 1990 |z 1

• 920 __ |a 261020 |b TP301-53 |c I61/1990 |z 1

• 920 __ |a 212020 |z 1

• 920 __ |a 251050 |z 1

• 920 __ |a 244050 |z 2

• 920 __ |a 232010 |z 1

• 920 __ |a 231010 |z 2

• 920 __ |a 231220 |z 1

• 920 __ |a 211010 |b TP3-5 |c L497/no.449 |z 1

• 950 __ |a 261060 |f TP18-53/E21:10th(90)

• 991 __022005003989

• 998 __ |a PUL

• 999 __ |t C |A shenxiaoyan |a 20050126 14:17:59 |M shenxiaoyan |m 20050126 14:18:34 |G shenxiaoyan |g 20050126 14:18:5