|
|
|
|
| LEADER |
00000nam a22000005i 4500 |
| 001 |
b3221494 |
| 003 |
MWH |
| 005 |
20191025172353.0 |
| 007 |
cr nn 008mamaa |
| 008 |
121227s2001 xxu| s |||| 0|eng d |
| 020 |
|
|
|a 9781461300892
|
| 024 |
7 |
|
|a 10.1007/978-1-4613-0089-2
|2 doi
|
| 035 |
|
|
|a (DE-He213)978-1-4613-0089-2
|
| 050 |
|
4 |
|a E-Book
|
| 072 |
|
7 |
|a PBC
|2 bicssc
|
| 072 |
|
7 |
|a MAT018000
|2 bisacsh
|
| 072 |
|
7 |
|a PBC
|2 thema
|
| 072 |
|
7 |
|a PBCD
|2 thema
|
| 100 |
1 |
|
|a Newborn, Monty.
|e author.
|4 aut
|4 http://id.loc.gov/vocabulary/relators/aut
|
| 245 |
1 |
0 |
|a Automated Theorem Proving
|h [electronic resource] :
|b Theory and Practice /
|c by Monty Newborn.
|
| 250 |
|
|
|a 1st ed. 2001.
|
| 264 |
|
1 |
|a New York, NY :
|b Springer New York :
|b Imprint: Springer,
|c 2001.
|
| 300 |
|
|
|a XIV, 231 p.
|b online resource.
|
| 336 |
|
|
|a text
|b txt
|2 rdacontent
|
| 337 |
|
|
|a computer
|b c
|2 rdamedia
|
| 338 |
|
|
|a online resource
|b cr
|2 rdacarrier
|
| 347 |
|
|
|a text file
|b PDF
|2 rda
|
| 490 |
1 |
|
|a Springer eBook Collection
|
| 505 |
0 |
|
|a A brief introduction to COMPILE, HERBY and THEO -- Predicate calculus, well-formed formulas and theorems -- COMPILE: transforming well-formed formulas to clauses -- Inference procedures -- Proving theorems by constructing closed semantic trees -- Resolution-refutation proofs -- HERBY: A semantic tree theorem prover -- Using HERBY -- THEO: A resolution-refutation theorem prover -- Using THEO -- A look at HERBY's source code -- A look at THEO's source code -- Other theorem provers -- References.
|
| 520 |
|
|
|a As the 21st century begins, the power of our magical new tool and partner, the computer, is increasing at an astonishing rate. Computers that perform billions of operations per second are now commonplace. Multiprocessors with thousands of little computers - relatively little! -can now carry out parallel computations and solve problems in seconds that only a few years ago took days or months. Chess-playing programs are on an even footing with the world's best players. IBM's Deep Blue defeated world champion Garry Kasparov in a match several years ago. Increasingly computers are expected to be more intelligent, to reason, to be able to draw conclusions from given facts, or abstractly, to prove theorems-the subject of this book. Specifically, this book is about two theorem-proving programs, THEO and HERBY. The first four chapters contain introductory material about automated theorem proving and the two programs. This includes material on the language used to express theorems, predicate calculus, and the rules of inference. This also includes a description of a third program included with this package, called COMPILE. As described in Chapter 3, COMPILE transforms predicate calculus expressions into clause form as required by HERBY and THEO. Chapter 5 presents the theoretical foundations of seman tic tree theorem proving as performed by HERBY. Chapter 6 presents the theoretical foundations of resolution-refutation theorem proving as per formed by THEO. Chapters 7 and 8 describe HERBY and how to use it.
|
| 590 |
|
|
|a Loaded electronically.
|
| 590 |
|
|
|a Electronic access restricted to members of the Holy Cross Community.
|
| 650 |
|
0 |
|a Mathematical logic.
|
| 650 |
|
0 |
|a Artificial intelligence.
|
| 690 |
|
|
|a Electronic resources (E-books)
|
| 710 |
2 |
|
|a SpringerLink (Online service)
|
| 773 |
0 |
|
|t Springer eBooks
|
| 830 |
|
0 |
|a Springer eBook Collection.
|
| 856 |
4 |
0 |
|u https://holycross.idm.oclc.org/login?auth=cas&url=https://doi.org/10.1007/978-1-4613-0089-2
|3 Click to view e-book
|
| 907 |
|
|
|a .b32214947
|b 04-18-22
|c 02-26-20
|
| 998 |
|
|
|a he
|b 02-26-20
|c m
|d @
|e -
|f eng
|g xxu
|h 0
|i 1
|
| 912 |
|
|
|a ZDB-2-SMA
|
| 912 |
|
|
|a ZDB-2-BAE
|
| 950 |
|
|
|a Mathematics and Statistics (Springer-11649)
|
| 902 |
|
|
|a springer purchased ebooks
|
| 903 |
|
|
|a SEB-COLL
|
| 945 |
|
|
|f - -
|g 1
|h 0
|j - -
|k - -
|l he
|o -
|p $0.00
|q -
|r -
|s b
|t 38
|u 0
|v 0
|w 0
|x 0
|y .i21346598
|z 02-26-20
|
| 999 |
f |
f |
|i 1faf838b-cbc0-5682-a621-da35454d1986
|s 5b5fa488-d347-5998-8908-a8cfb8c21c8a
|
| 952 |
f |
f |
|p Online
|a College of the Holy Cross
|b Main Campus
|c E-Resources
|d Online
|e E-Book
|h Library of Congress classification
|i Elec File
|n 1
|