Handbook of Automated Reasoning

Zusammenfassung This first volume of the "Handbook of Automated Reasoning" includes topics such as: the early history of automated deduction, classical logic - resolution theorem proving, and tableaux and related methods.

Sommario

Part I. History 1. The Early History of Automated Deduction (Martin Davis)
Part II. Classical Logic. 2. Resolution Theorem Proving (Leo Bachmair, Harald Ganzinger) 3. Tableaux and Related Methods (Reiner Hähnle) 4. The Inverse Method (Anatoli Degtyarev, Andrei Voronkov) 5. Normal Form Transformations (Matthias Baaz, Uwe Egly, Alexander Leitsch) 6. Computing Small Clause Normal Forms (Andreas Nonnengart, Christoph Weidenbach)
Part III. Equality and other theories. 7. Paramodulation-Based Theorem Proving (Robert Nieuwenhuis, Albert Rubio) 8. Unification Theory (Franz Baader, Wayne Snyder) 9. Rewriting (Nachum Dershowitz, David A. Plaisted) 10. Equality Reasoning in Sequent-Based Calculi (Anatoli Degtyarev, Andrei Voronkov) 11. Automated Reasoning in Geometry (Shang-Ching Chou, Xiao-Shan Gao) 12. Solving Numerical Constraints (Alexander Bockmayr, Volker Weispfenning)
Part IV. Induction. 13. The Automation of Proof by Mathematical Induction (Alan Bundy) 14. Inductionless Induction (Hubert Comon)

Dettagli sul prodotto

• Autori: Robinson, A. Robinson, A. Voronkov
• Con la collaborazione di: Alan Robinson (Editore), Alan J. a. Robinson (Editore), Alan J.A. (96 Highland Avenue Robinson (Editore), Andrei Voronkov (Editore), Andrei (University of Manchester Voronkov (Editore)
• Editore: ELSEVIER SCIENCE BV
• Lingue: Inglese
• Formato: Copertina rigida
• Pubblicazione: 21.06.2001
• EAN: 9780444829498
• ISBN: 978-0-444-82949-8
• Pagine: 996
• Serie: Handbook of Automated Reasoning
• Categoria: Scienze naturali, medicina, informatica, tecnica > Informatica, EDP > Informatica