## Handbook of Automated Reasoning, Volume 2 (Google eBook)Handbook of Automated Reasoning |

### What people are saying - Write a review

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

### Contents

Encoding consequence relations | 1419 |

The functional translation | 1440 |

Conclusion | 1475 |

Connections in Nonclassical Logics | 1487 |

Labelled systems | 1516 |

Firstorder intuitionistic logic | 1545 |

The S5 family | 1567 |

Reasoning in Expressive Description Logics | 1581 |

168 | |

181 | |

209 | |

strategies and redundancies | 232 |

Logics without the contraction rules | 255 |

Conclusion | 260 |

HANDBOOK OF AUTOMATED REASONING | 264 |

Normal Form Transformations | 273 |

On the Concept of Normal Form | 287 |

Conjunctive Normal Form | 306 |

Normal Forms in Nonclassical Logics | 323 |

Computing Small Clause Normal Forms | 335 |

ParamodulationBased Theorem Proving | 371 |

Paramodulation calculi | 385 |

Saturation procedures | 399 |

Paramodulation with constrained clauses | 414 |

Paramodulation with builtin equational theories | 421 |

Extensions | 427 |

Index | 440 |

Unification Theory | 445 |

Equational unification | 469 |

Syntactic methods for unification | 488 |

Semantic approaches to Eunification | 503 |

Further topics | 519 |

Rewriting | 535 |

ChurchRosser Properties | 559 |

Relativized Rewriting | 574 |

Programming | 593 |

Equality Reasoning in SequentBased Calculi | 611 |

Translation of logic with equality into logic without equality | 628 |

Early history | 644 |

Sequentbased calculi and paramodulation | 660 |

Equality reasoning in nonclassical logics | 679 |

Automated Reasoning in Geometry | 707 |

Coordinatefree approaches to automated reasoning in geometry | 732 |

Solving Numerical Constraints | 751 |

The Automation of Proof by Mathematical | 845 |

The Productive Use of Failure | 890 |

Interactive Theorem Proving | 898 |

Inductionless Induction | 913 |

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 |

Concept Index | 963 |

Higherorder logic and logical frameworks | xiv |

Further topics 519 | xvii |

Classical Type Theory 965 | 965 |

Proof search | 987 |

HigherOrder Unification and Matching | 1009 |

Undecidability | 1024 |

Decidable Subcases | 1041 |

Logical Frameworks | 1063 |

ProofAssistants Using Dependent Type Systems | 1149 |

Towards Efficient | 1241 |

Automated Deduction for ManyValued Logics | 1355 |

reasoning classically about finitelyvalued logics | 1368 |

An example | 1389 |

Encoding TwoValued Nonclassical Logics | 1403 |

Unrestricted Model Reasoning | 1598 |

Beyond Basic Description Logics | 1619 |

Model Checking | 1635 |

Second Order Languages | 1654 |

Model Transformations and Properties | 1670 |

Completeness | 1689 |

Basic Model Checking Algorithms | 1711 |

Modelling of Reactive Systems | 1724 |

Symbolic Model Checking | 1735 |

Partial Order Techniques | 1751 |

Bounded Model Checking | 1755 |

Abstractions | 1759 |

Compositionality and Modular Verification | 1764 |

Further Topics | 1767 |

1774 | |

1788 | |

Resolution Decision Procedures | 1791 |

Introduction | 1793 |

Notation and definitions | 1794 |

Decision procedures based on ordering refinements | 1802 |

Hyperresolution as decision procedure | 1814 |

Resolution decision procedures for description logics | 1830 |

Related work | 1842 |

Bibliography | 1843 |

1847 | |

Implementation | 1851 |

Term Indexing | 1853 |

R Sekar I V Ramakrishnan and Andrei Voronkov 1 Introduction | 1855 |

Background | 1859 |

Data structures for representing terms and indexes | 1866 |

A common framework for indexing | 1870 |

Path indexing | 1875 |

Discrimination trees | 1883 |

Adaptive automata | 1891 |

Automatadriven indexing | 1900 |

Code trees | 1908 |

Substitution trees | 1917 |

Context trees | 1922 |

Unification factoring | 1924 |

Multiterm indexing | 1927 |

Issues in perfect filtering | 1934 |

Indexing modulo ACtheories | 1939 |

Elements of term indexing | 1943 |

Indexing in practice | 1951 |

Conclusion | 1955 |

Combining Superposition Sorts and Splitting | 1965 |

A First Simple Prover | 1973 |

Inference and Reduction Rules | 1981 |

Global Design Decisions | 2000 |

2011 | |

Tableau Procedures | 2017 |

Further Structural Refinements of Clausal Tableaux | 2036 |

Shortening of Proofs | 2049 |

Completeness of Connection Tableaux | 2062 |

Architectures of Model Elimination Implementations | 2070 |

Implementation of Refinements by Constraints | 2092 |

Experimental Results | 2102 |

2109 | |

2115 | |

### Common terms and phrases

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