default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDHandbook of Automated Reasoning, 2001
- John Alan Robinson, Andrei Voronkov:
Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press 2001, ISBN 0-444-50813-9
Volume 1
- John Alan Robinson, Andrei Voronkov:
Preface. v-vii
- Martin Davis:
The Early History of Automated Deduction. 3-15
- Leo Bachmair, Harald Ganzinger:
Resolution Theorem Proving. 19-99
- Reiner Hähnle
:
Tableaux and Related Methods. 100-178
- Anatoli Degtyarev, Andrei Voronkov:
The Inverse Method. 179-272
- Matthias Baaz, Uwe Egly, Alexander Leitsch:
Normal Form Transformations. 273-333
- Andreas Nonnengart, Christoph Weidenbach:
Computing Small Clause Normal Forms. 335-367
- Robert Nieuwenhuis, Albert Rubio:
Paramodulation-Based Theorem Proving. 371-443
- Franz Baader, Wayne Snyder:
Unification Theory. 445-532
- Nachum Dershowitz, David A. Plaisted:
Rewriting. 535-610
- Anatoli Degtyarev, Andrei Voronkov:
Equality Reasoning in Sequent-Based Calculi. 611-706
- Shang-Ching Chou, Xiao-Shan Gao:
Automated Reasoning in Geometry. 707-749
- Alexander Bockmayr, Volker Weispfenning:
Solving Numerical Constraints. 751-842
- Alan Bundy:
The Automation of Proof by Mathematical Induction. 845-911
- Hubert Comon:
Inductionless Induction. 913-962
Volume 2
- Peter B. Andrews:
Classical Type Theory. 965-1007
- Gilles Dowek:
Higher-Order Unification and Matching. 1009-1062
- Frank Pfenning:
Logical Frameworks. 1063-1147
- Henk Barendregt, Herman Geuvers:
Proof-Assistants Using Dependent Type Systems. 1149-1238
- Jürgen Dix, Ulrich Furbach, Ilkka Niemelä:
Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations. 1241-1354
- Matthias Baaz, Christian G. Fermüller, Gernot Salzer:
Automated Deduction for Many-Valued Logics. 1355-1402
- Hans Jürgen Ohlbach, Andreas Nonnengart, Maarten de Rijke, Dov M. Gabbay:
Encoding Two-Valued Nonclassical Logics in Classical Logic. 1403-1486
- Arild Waaler:
Connections in Nonclassical Logics. 1487-1578
- Diego Calvanese, Giuseppe De Giacomo, Daniele Nardi, Maurizio Lenzerini:
Reasoning in Expressive Description Logics. 1581-1634
- Edmund M. Clarke, Bernd-Holger Schlingloff:
Model Checking. 1635-1790
- Christian G. Fermüller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet:
Resolution Decision Procedures. 1791-1849
- I. V. Ramakrishnan, R. Sekar, Andrei Voronkov:
Term Indexing. 1853-1964
- Christoph Weidenbach:
Combining Superposition, Sorts and Splitting. 1965-2013
- Reinhold Letz, Gernot Stenz:
Model Elimination and Connection Tableau Procedures. 2015-2114
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-11-18 22:32 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
