|
020 -INTERNATIONAL STANDARD BOOK NUMBER
|
|
|
|
040 -CATALOGING SOURCE
|
|
a
Original cataloging agency
NEU GrandLibrary
|
|
|
050 -LIBRARY OF CONGRESS CALL NUMBER
|
|
a
Classification number
QA76.9.A96
|
|
b
Item number
K35 2001
|
|
|
082 -DEWEY DECIMAL CLASSIFICATION NUMBER
|
|
a
Dewey Classification
006.3/33
|
|
|
100 -MAIN ENTRY--PERSONAL NAME
|
|
a
Personal name
Kalman John Arnold
|
|
|
245 -TITLE STATEMENT
|
|
a
Title
Automated reasoning with Otter /
|
|
c
Statement of responsibility, etc
John Arnold Kalman ; with a foreword by Larry Wos.
|
|
h
Medium
Book&CD
|
|
|
260 -PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
|
|
a
Place of publication, distribution, etc
Princeton, N.J. :
|
|
b
Name of publisher, distributor, etc
Rinton Press,
|
|
c
Date of publication, distribution, etc
2001.
|
|
|
300 -PHYSICAL DESCRIPTION
|
|
a
Extent
xv, 536 p. ;
|
|
c
Dimensions
27 cm. +
|
|
|
500 -GENERAL NOTE
|
|
a
General note
Includes index.
|
|
|
650 -SUBJECT ADDED ENTRY--TOPICAL TERM
|
|
a
Topical term or geographic name as entry element
Automatic theorem proving
|
|
|
650 -SUBJECT ADDED ENTRY--TOPICAL TERM
|
|
a
Topical term or geographic name as entry element
Artificial intelligence
|
|
|
650 -SUBJECT ADDED ENTRY--TOPICAL TERM
|
|
a
Topical term or geographic name as entry element
Computer programming
|
|
