Handbook of Automated Reasoning, Volume 1

Front Cover
Gulf Professional Publishing, Jan 1, 2001 - Computers - 2122 pages
0 Reviews
This first volume of the Handbook of Automated Reasoning includes topics such as: the early history of automated deduction, classical logic - resolution theorem proving, and tableaux and related methods.
  

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

David McAllester and Christopher Lynch
21
FirstOrder Resolution Methods
89
HANDBOOK OF AUTOMATED REASONING
94
TABLEAUX AND RELATED METHODS
101
Clause Tableaux
125
Tableaux as a Framework
152
Historical Remarks Resources
167
Nonclassical logics
175
Description Logics 1586
521
What This Chapter is not About 1967
525
REWRITING
535
ChurchRosser Properties
559
Relativized Rewriting
574
Programming
593
Outlook 2107
597
EQUALITY REASONING IN SEQUENTBASED CALCULI
611

Introduction
181
Applying the recipe to nonclassical logics
209
strategies and redundancies
232
Logics without the contraction rules
255
Modelling of Reactive Systems 1724
259
Higherorder logic and logical frameworks
264
Bounded Model Checking 1755
265
TOWARDS EFFICIENT
266
NORMAL FORM TRANSFORMATIONS
273
On the Concept of Normal Form
287
Conjunctive Normal Form
306
What is a manyvalued logic? 1358
307
Normal Forms in Nonclassical Logics
323
Optimization of transformation rules 1393
328
CONNECTIONS IN NONCLASSICAL LOGICS 1487
331
COMPUTING SMALL CLAUSE NORMAL FORMS
335
PARAMODULATIONBASED THEOREM PROVING
371
Paramodulation calculi
385
Saturation procedures
399
Paramodulation with constrained clauses
414
Extensions
427
UNIFICATION THEORY
445
Equational unification
469
Syntactic methods for unification
488
Semantic approaches to unification
503
Further topics
519
Translation of logic with equality into logic without equality
628
Early history
644
Sequentbased calculi and paramodulation
660
Equality reasoning in nonclassical logics
679
Abstractions 1759
685
HIGHERORDER UNIFICATION AND MATCHING 1009
696
AUTOMATED REASONING IN GEOMETRY
707
Coordinatefree approaches to automated reasoning in geometry
732
Huets Algorithm 1028
741
SOLVING NUMERICAL CONSTRAINTS
751
THE AUTOMATION OF PROOF BY MATHEMATICAL
845
RESOLUTION DECISION PROCEDURES 1791
905
INDUCTIONLESS INDUCTION
913
Notation and definitions 1794
914
Introduction 1855
915
Background 1859
918
Formal background
919
General Setting of the Inductionless Induction Method
925
Examples of Axiomatizations A from the Literature
938
Ground Reducibility
948
A comparison between inductive proofs and proofs by consistency
957
Data structures for representing terms and indexes 1866
960
Concept Index
963
Description Logics and Prepositional Dynamic Logics 1593
965
PROOFASSISTANTS USING DEPENDENT TYPE SYSTEMS 1149
967
Copyright

Common terms and phrases

Popular passages

Page 824 - M.-F. ROY A New Algorithm to Find a Point in Every Cell Defined by a Family of Polynomials in "Quantifier Elimination and Cylindrical Algebraic Decomposition", B.

References to this book

All Book Search results »

About the author (2001)

Alan G. Robinson is a professor at the Isenberg School of Management at the University of Massachusetts, Amherst. Robinson and Schroeder have advised hundreds of organizations in more than twenty-five countries on how to improve their performance.

Andrei Voronkov is Professor of Computer Science at the University of Manchester, UK.

Bibliographic information