Handbook of Automated Reasoning, Volume 2

Front Cover
John Alan Robinson, Andreĭ Voronkov
Elsevier, Jan 1, 2001 - Computers - 2122 pages
0 Reviews
This 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
Index
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
Index
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
Conditional Rewriting 585
2115
Formal background 919
2117
Copyright

Common terms and phrases

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