The ''Handbook of Automated Reasoning'' (, 2128 pages) is a collection of survey articles on the field of

automated reasoning In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer prog ...

. Published in June 2001 by

MIT Press The MIT Press is a university press affiliated with the Massachusetts Institute of Technology (MIT) in Cambridge, Massachusetts (United States). It was established in 1962. History The MIT Press traces its origins back to 1926 when MIT publish ...

, it is edited by

John Alan Robinson John Alan Robinson (9 March 1930 – 5 August 2016) was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University. Alan Robinson's major contribution is to the foundations of automated theorem pr ...

and

Andrei Voronkov Andrei Anatolievič Voronkov (born 1959) is a Professor of Formal methods in the Department of Computer Science at the University of Manchester. Education Voronkov was educated at Novosibirsk State University, graduating with a PhD in 1987. Res ...

. Volume 1 describes methods for classical logic,

first-order logic with equality In mathematics and other formal sciences, first-order or first order most often means either: * "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of hi ...

and other theories, and

induction Induction, Inducible or Inductive may refer to: Biology and medicine * Labor induction (birth/pregnancy) * Induction chemotherapy, in medicine * Induced stem cells, stem cells derived from somatic, reproductive, pluripotent or other cell t ...

. Volume 2 covers higher-order, non-classical and other kinds of logic.

Index

Volume 1

;History ;Classical Logic ;Equality and Other Theories ;Induction

Volume 2

;Higher-Order Logic and Logical Frameworks ;Nonclassical Logics ;Decidable Classes and Model Building ;Implementation {{Ordered list , start=26 , I.V. Ramakrishnan, R.Sekar,

. Term Indexing, pp. 1853–1964. ,

Christoph Weidenbach Christoph is a male given name and surname. It is a German variant of Christopher. Notable people with the given name Christoph * Christoph Bach (1613–1661), German musician * Christoph Büchel (born 1966), Swiss artist * Christoph Dientzenho ...

. Combining Superposition, Sorts and Splitting, pp. 1965–2013. , Reinhold Letz, Gernot Stenz. Model Elimination and Connection Tableau Procedures, pp. 2015–2114.

External links

MIT press page
2001 non-fiction books Handbooks and manuals Logic books Computer science books Automated reasoning