Monty Newborn

Automated Theorem Proving (eBook, PDF)

Theory and Practice

• Format: PDF

Produktbeschreibung

This new book carefully describes how automated reasoning is performed. It introduces all necessary analytical and mathematical tools to discuss basic inference rules of binary resolution and binary factoring. Two computer programs and source code are provided to use as examples. Advanced students, professionals and researchers in computer science, computer engineering, artificial intelligence and logic programming will find the book a useful text/reference.

---

Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.

Produktdetails

• Verlag: Springer US
• Seitenzahl: 231
• Erscheinungstermin: 6. Dezember 2012
• Englisch
• ISBN-13: 9781461300892
• Artikelnr.: 43992303

Inhaltsangabe

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.