A many-sorted calculus based on resolution and paramodulation

Main Author: Walther, Christoph.
Other Authors: ScienceDirect (Online service)
Format: eBook
Language: English
German
Published: London : Los Altos, Calif. : Pitman ; Morgan Kaufmann Publishers, 1987.
Physical Description: 1 online resource (160 pages) : illustrations.
Series: Research notes in artificial intelligence (London, England)
Subjects:
LEADER 03827cam a2200829Ka 4500
001 574434431
003 OCoLC
005 20210116033556.6
006 m o d
007 cr bn||||||abp
007 cr bn||||||ada
008 100325s1987 enka ob 000 0 eng d
019 |a 776606882  |a 974614441  |a 974664198  |a 1036606118 
020 |a 9780273087182  |q (electronic bk.) 
020 |a 0273087185  |q (electronic bk.) 
020 |z 0934613494  |q (Morgan Kaufmann ;  |q pbk.) 
020 |z 9780934613491  |q (Morgan Kaufmann ;  |q pbk.) 
035 |a (OCoLC)574434431  |z (OCoLC)776606882  |z (OCoLC)974614441  |z (OCoLC)974664198  |z (OCoLC)1036606118 
040 |a OCLCE  |b eng  |e pn  |c OCLCE  |d OCLCQ  |d OCLCF  |d OCLCO  |d OCLCQ  |d OPELS  |d OCLCQ  |d INARC  |d OCLCO  |d OCLCQ  |d LUN  |d OCLCQ 
041 1 |a eng  |h ger 
042 |a dlr 
049 |a COM6 
050 4 |a QA76.9.A96  |b W35 1987 
082 0 4 |a 511.3/0285  |2 19 
084 |a 54.72  |2 bcl 
084 |a *68T15  |2 msc 
084 |a 03B10  |2 msc 
084 |a 03B35  |2 msc 
084 |a 68-02  |2 msc 
084 |a SK 130  |2 rvk 
084 |a ST 285  |2 rvk 
084 |a DAT 706d  |2 stub 
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 1 online resource (160 pages) :  |b illustrations. 
336 |a text  |b txt  |2 rdacontent. 
337 |a computer  |b c  |2 rdamedia. 
338 |a online resource  |b cr  |2 rdacarrier. 
490 1 |a Research notes in artificial intelligence,  |x 0268-7526. 
504 |a Includes bibliographical references (pages 154-160). 
506 |3 Use copy  |f Restrictions unspecified  |2 star  |5 MiAaHDL. 
533 |a Electronic reproduction.  |b [S.l.] :  |c HathiTrust Digital Library,  |d 2010.  |5 MiAaHDL. 
538 |a Master and use copy. Digital master created according to Benchmark for Faithful Digital Reproductions of Monographs and Serials, Version 1. Digital Library Federation, December 2002.  |u http://purl.oclc.org/DLF/benchrepro0212  |5 MiAaHDL. 
583 1 |a digitized  |c 2010  |h HathiTrust Digital Library  |l committed to preserve  |2 pda  |5 MiAaHDL. 
588 0 |a Print version record. 
650 0 |a Automatic theorem proving. 
650 0 |a Artificial intelligence. 
650 6 |a Théorèmes  |x Démonstration automatique. 
650 6 |a Intelligence artificielle. 
650 7 |a Artificial intelligence.  |2 fast. 
650 7 |a Automatic theorem proving.  |2 fast. 
650 7 |a Mehrsortige Prädikatenlogik.  |2 gnd. 
650 7 |a Automatisches Beweisverfahren.  |2 gnd. 
650 7 |a Künstliche Intelligenz.  |2 gnd. 
650 1 7 |a Kunstmatige intelligentie.  |2 gtt. 
650 1 7 |a Redeneren.  |2 gtt. 
650 1 7 |a Bewijs (wetenschap)  |2 gtt. 
653 |a Theorems  |a Proof  |a Applications of computer systems. 
655 4 |a Electronic books. 
710 2 |a ScienceDirect (Online service) 
776 0 8 |i Print version:  |a Walther, Christoph.  |t Many-sorted calculus based on resolution and paramodulation.  |d London : Pitman ; Los Altos, Calif. : Morgan Kaufmann Publishers, 1987  |w (DLC) 87002815  |w (OCoLC)15591420. 
830 0 |a Research notes in artificial intelligence (London, England) 
907 |a .b63758775  |b multi  |c -  |d 210303  |e 230217 
998 |a cue  |a cu  |b 210303  |c m  |d z   |e -  |f eng  |g enk  |h 2  |i 1 
948 |a MARCIVE Comprehensive, in 2023.02 
948 |a MARCIVE Over, 04/2021 
994 |a 92  |b COM 
995 |a Loaded with m2btab.ltiac in 2023.02 
995 |a Loaded with m2btab.ltiac in 2021.04 
995 |a Loaded with m2btab.elec in 2021.03 
989 |d cueme  |e  - -   |f  - -   |g j   |h 0  |i 0  |j 188  |k 210303  |l $0.00  |m    |n  - -   |o -  |p 0  |q 0  |t 0  |x 0  |w Elsevier  |1 .i13670167x  |u http://ezproxy.coloradomesa.edu/login?url=https://www.sciencedirect.com/science/book/9780273087182  |3 Elsevier  |z Click here for access