Robinson A., Voronkov A. (eds.) Handbook of Automated Reasoning. Volume II

Elsevier/MIT Press, 2001. — 1171 p.This Handbook presents overviews of the fundamental notions, techniques, ideas, and methods developed and used in automated reasoning and its applications, which are used in many areas of computer science, including software and hardware verification, logic and functional programming, formal methods, knowledge representation, deductive databases, and artificial intelligence.Part V Higher-Order Logic and Logical Frameworks
Classical Type Theory
Higher-Order Unification and Matching
Logical Frameworks
Proof-Assistants Using Dependent Type Systems
Part VI Nonclassical Logics
Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations
Automated Deduction for Many-Valued Logics
Encoding Two-Valued Nonclassical Logics in Classical Logic
Connections in Nonclassical Logics
Part VII Decidable Classes and Model Building
Reasoning in Expressive Description Logics
Model Checking
Resolution Decision Procedures
Part VIII Implementation
Term Indexing
Combining Superposition, Sorts and Splitting
Model Elimination and Connection Tableau Procedures