A many-sorted calculus based on resolution and paramodulation /

Bibliographic Details
Main Author: Walther, Christoph
Format: Book
Language:English
German
Published: London : Los Altos, Calif. : Pitman ; Morgan Kaufmann Publishers, 1987.
Series:Research notes in artificial intelligence (London, England)
Subjects:

MARC

Tag First Indicator Second Indicator Subfields
LEADER 00000cam a2200000 a 4500
001 in00000026825
005 20151007054548.0
008 870407s1987 enka b 00010 eng
010 |a  87002815  
020 |a 0934613494 (Morgan Kaufmann : pbk.) :  |c $22.95 
035 |a (OCoLC)15591420 
035 |9 AAB5510AM 
040 |a DLC  |c DLC  |d TXA  |d UtOrBLW 
041 1 |a eng  |a ger 
049 |a TXAM  |c [A10909481] 
050 0 0 |a QA76.9.A96  |b W35 1987 
082 0 |a 511.3  |2 19 
100 1 |a Walther, Christoph. 
245 1 2 |a A many-sorted calculus based on resolution and paramodulation /  |c Christoph Walther. 
264 1 |a London :  |b Pitman ;  |a Los Altos, Calif. :  |b Morgan Kaufmann Publishers,  |c 1987. 
300 |a 160 pages :  |b illustrations ;  |c 25 cm. 
336 |a text  |b txt  |2 rdacontent 
337 |a unmediated  |b n  |2 rdamedia 
338 |a volume  |b nc  |2 rdacarrier 
490 1 |a Research notes in artificial intelligence,  |x 0268-7526 
500 |a Revised translation of thesis (doctoral)--University of Karlsruhe, 1984. 
504 |a Bibliography: pages 154-160. 
650 0 |a Automatic theorem proving. 
650 0 |a Artificial intelligence. 
830 0 |a Research notes in artificial intelligence (London, England) 
999 |a MARS 
999 f f |s 36fc17cb-81c3-3398-ac5d-60737a30f9fc  |i f69938e1-2e5f-3c3d-ac29-c544821e4aaa  |t 0 
952 f f |p ric  |a Texas A&M University  |b Rellis Campus  |c Joint Library Facility  |d Remote Storage  |t 0  |e QA76.9.A96 W35 1987  |h Library of Congress classification  |i unmediated -- volume  |m A14810909481 
998 f f |a QA76.9.A96 W35 1987  |t 0  |l Remote Storage