## Handbook of Automated Reasoning, Volume 1This 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 |

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 |

960 | |

963 | |

965 | |

967 | |

### Common terms and phrases

algebraic algorithm applied Artificial Intelligence atom Automated Deduction Automated Reasoning axioms Bachmair branch calculus chapter complete Computer Science consider constraint contains critical pair defined DEFINITION denote derivation Dershowitz E-unification elimination equality equational theory equivalent example finite first-order first-order logic free variables function symbols Ganzinger geometry ground instances Handbook of Automated Herbrand Horn clauses induction rule inference rules inference system intuitionistic logic inverse method Kapur Lecture Notes lemma linear literals minimal modal logics multiset negation normal form Nieuwenhuis normal form Notes in Computer obtained occur paramodulation path ordering polynomial positive predicate premises programming proof quantifier elimination quantifiers recursive redundant refutation renaming restrictions rewrite rules rewrite system Robinson satisfiable saturated Section semantic sequent calculus set of clauses signed formulas simplification simultaneous rigid Skolem solution Springer-Verlag step subformula substitution subterm superposition tableau techniques termination theorem proving transformation unification problem unifier unsatisfiable

### 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.