Handbook of Automated Reasoning

Automated reasoning has matured into one of the most advanced areas ofcomputer science. It is used in many areas of the field, including software andhardware verification, logic and functional programming, formal methods, knowledgerepresentation, deductive databases, and artificial intelligence. This handbookpresents an overview of the fundamental ideas, techniques, and methods in automatedreasoning and its applications. The material covers both theory and implementation.In addition to traditional topics, the book covers material that bridges the gapbetween automated reasoning and related areas. Examples include model checking, nonmonotonic reasoning, numerical constraints, description logics, andimplementation of declarative programming languages.The book consists of eightparts. After an overview of the early history of automated deduction, the areascovered are reasoning methods in first-order logic; equality and other built-intheories; methods of automated reasoning using induction; higher-order logic, whichis used in a number of automatic and interactive proof-development systems;automated reasoning in nonclassical logics; decidable classes and model building;and implementation-related questions.