×

zbMATH — the first resource for mathematics

Handbook of automated reasoning. In 2 vols. (English) Zbl 0964.00020
Amsterdam: North-Holland/ Elsevier; 0-444-50812-0 (vol. 2); 0-444-50813-9 (set)). Cambridge, MA: MIT Press; 0-262-18222-X (vol. 2); 0-262-18223-8 (set)). xxv, 2122 p. (2001).

Show indexed articles as search result.

Publisher’s description: A comprehensive resource on automated reasoning and its applications. Automated reasoning has matured into one of the most advanced areas of computer science. It is used in many areas of the field, including software and hardware verification, logic and functional programming, formal methods, knowledge representation, deductive databases, and artificial intelligence. This handbook presents an overview of the fundamental ideas, techniques, and methods in automated reasoning and its applications. The material covers both theory and implementation. In addition to traditional topics, the Handbook contains material that bridges the gap between automated reasoning and related areas. Examples are model checking, nonmonotonic reasoning, numerical constraints, description logics, and implementation of declarative programming languages.
The book consists of eight parts. After an overview of the early history of automated deduction, the areas covered are reasoning methods in first-order logic; equality and other built-in theories; methods of automated reasoning using induction; higher-order logic, which is 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. The articles of this volume will be reviewed individually.
Indexed articles:
Davis, Martin, The early history of automated deduction, 4-15 [Zbl 1011.68511]
Bachmair, Leo; Ganzinger, Harald, Resolution theorem proving, 19-99 [Zbl 0993.03008]
Hähnle, Reiner, Tableaux and related methods, 101-178 [Zbl 1011.68125]
Degtyarev, Anatoli; Voronkov, Andrei, The inverse method, 179-272 [Zbl 0992.03016]
Baaz, Matthias; Egly, Uwe; Leitsch, Alexander, Normal form transformations, 273-333 [Zbl 1005.03013]
Nonnengart, Andreas; Weidenbach, Christoph, Computing small clause normal forms, 335-367 [Zbl 0992.03018]
Nieuwenhuis, Robert; Rubio, Albert, Paramodulation-based theorem proving, 371-443 [Zbl 0997.03012]
Baader, Franz; Snyder, Wayne, Unification theory, 445-533 [Zbl 1011.68126]
Dershowitz, Nachum; Plaisted, David A., Rewriting, 535-610 [Zbl 0992.68123]
Degtyarev, Anatoli; Voronkov, Andrei, Equality reasoning in sequent-based calculi, 611-706 [Zbl 1011.03004]
Chou, Shang-Ching; Gao, Xiao-Shan, Automated reasoning in geometry, 707-749 [Zbl 1011.68128]
Bockmayr, Alexander; Weispfenning, Volker, Solving numerical constraints, 751-842 [Zbl 1011.68127]
Bundy, Alan, The automation of proof by mathematical induction, 845-911 [Zbl 0994.03007]
Comon, Hubert, Inductionless induction, 913-960 [Zbl 0994.03006]
Andrews, Peter B., Classical type theory, 965-1007 [Zbl 0992.03011]
Dowek, Gilles, Higher-order unification and matching, 1009-1062 [Zbl 1011.03005]
Pfenning, Frank, Logical frameworks, 1063-1147 [Zbl 0992.03038]
Barendregt, Henk; Geuvers, Herman, Proof-assistants using dependent type systems, 1149-1238 [Zbl 1005.03011]
Dix, Jürgen; Furbach, Ulrich; Niemelä, Ilkka, Nonmonotonic reasoning: Towards efficient calculi and implementations, 1241-1354 [Zbl 0991.03036]
Baaz, Matthias; Fermüller, Christian G.; Salzer, Gernot, Automated deduction for many-valued logics, 1355-1402 [Zbl 0992.03015]
Ohlbach, Hans Jürgen; Nonnengart, Andreas; de Rijke, Maarten; Gabbay, Dov M., Encoding two-valued nonclassical logics in classical logic, 1403-1486 [Zbl 0992.03019]
Waaler, Arild, Connections in nonclassical logics, 1487-1578 [Zbl 0992.03020]
Calvanese, Diego; De Giacomo, Giuseppe; Nardi, Daniele; Lenzerini, Maurizio, Reasoning in expressive description logics, 1581-1634 [Zbl 0992.03036]
Clarke, Edmund M.; Schlingloff, Bernd-Holger, Model checking., 1635-1790 [Zbl 1066.68075]
Fermüller, Christian G.; Leitsch, Alexander; Hustadt, Ullrich; Tammet, Tanel, Resolution decision procedures, 1791-1849 [Zbl 0993.68119]
Sekar, R.; Ramakrishnan, I. V.; Voronkov, Andrei, Term indexing, 1853-1964 [Zbl 0992.68189]
Weidenbach, Christoph, Combining superposition, sorts and splitting, 1965-2013 [Zbl 1011.68129]
Letz, Reinhold; Stenz, Gernot, Model elimination and connection tableau procedures, 2015-2114 [Zbl 1011.68130]

MSC:
00B15 Collections of articles of miscellaneous specific interest
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68-00 General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science
PDF BibTeX Cite