## Handbook of Automated Reasoning, Volume 2This second volume of Handbook of Automated Reasoning covers topics such as higher-order logic and logical frameworks, higher-order unification and matching, logical frameworks, proof-assistants using dependent type systems, and nonclassical logics. |

### What people are saying - Write a review

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

### Contents

Solving Numerical Constraints 751 | 967 |

Metatheoretical foundations | 977 |

Conclusion | 998 |

Preliminaries 104 | 999 |

Type Theory and Other Set Theories | 1011 |

Induction | 1020 |

Undecidability | 1024 |

Decidable Subcases | 1041 |

1788 | |

Notation and Definitions 278 | 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 |

Normal Forms in Nonclassical Logics 323 | 1840 |

Unification in Acalculus with Dependent Types | 1049 |

Alan Bundy | 1054 |

1061 | |

Logical Frameworks | 1063 |

Terminology 541 | 1075 |

The Inverse Method 179 | 1096 |

Preliminaries 185 | 1138 |

ProofAssistants Using Dependent Type Systems | 1149 |

Towards Efficient | 1241 |

Automating General Nonmonotonic Logics | 1260 |

From Automated Reasoning to Disjunctive Logic Programming | 1280 |

Nonmonotonic Semantics of Logic Programs | 1297 |

Implementing Nonmonotonic Semantics | 1311 |

Benchmarks | 1332 |

Volume 1 | 1344 |

Automated Deduction for ManyValued Logics | 1355 |

History | 1357 |

Normal Forms and Validity 544 | 1363 |

reasoning classically about finitelyvalued logics | 1368 |

An example | 1389 |

Classical Logic | 1403 |

Normal Form Transformations 273 | 1428 |

Introduction 275 | 1455 |

Inductionless Induction 913 | 1478 |

Computing Small Clause Normal Forms 335 | 1481 |

Connections in Nonclassical Logics | 1487 |

Termination Properties 546 | 1515 |

Labelled systems | 1516 |

Firstorder intuitionistic logic | 1545 |

The S5 family | 1567 |

Reasoning in Expressive Description Logics | 1581 |

Unrestricted Model Reasoning | 1598 |

Beyond Basic Description Logics | 1619 |

Model Checking | 1635 |

ChurchRosser Properties 559 | 1639 |

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 |

Bibliography | 1774 |

Related work | 1842 |

Relativized Rewriting 574 | 1843 |

Index | 1847 |

Implementation | 1851 |

Term Indexing | 1853 |

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 |

Equality and other theories | 1959 |

Combining Superposition Sorts and Splitting | 1965 |

A First Simple Prover | 1973 |

Inference and Reduction Rules | 1981 |

Global Design Decisions | 2000 |

A Links to Saturation Based Provers | 2011 |

About this chapter 373 | 2015 |

Introduction | 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 |

Paramodulation with constrained clauses 414 | 2093 |

Experimental Results | 2102 |

Paramodulation with builtin equational theories 421 | 2109 |

2115 | |

2117 | |

### Common terms and phrases

A-calculus AHOL algorithm applied Artificial Intelligence atomic autoepistemic autoepistemic logic Automated Deduction Automated Reasoning automated theorem proving axiom binary calculus circumscription clause set completeness Computer Science construct context default logic default theory defined Definition denotes derivation Dowek encoding equation equivalent example expansion extension extensionality finite first-order logic free variables function Herbrand higher-order logic higher-order unification Huet implementation inference rules introduced intuitionistic judgments language Lecture Notes Lemma literals Logic Programming logical framework mathematical method minimal model modal logic model elimination natural deduction natural numbers negation Niemela node nonmonotonic reasoning normal form occur Pfenning F predicate logic procedure proof search proof-assistants Prop propositional quantifiers relation representation resolution Section semantic tree semantics sequent sequent calculus setoid signed formula expressions Skolem solution Springer-Verlag stable model substitution tableau term theorem proving translation tree truth values type system type theory unification problem unifier University