Handbook of Automated Reasoning, Volume 2 (Google eBook)

Front Cover
Alan J.A. Robinson, Andrei Voronkov
Elsevier, Jun 22, 2001 - Computers - 2128 pages
0 Reviews
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

HANDBOOK OF AUTOMATED REASONING
168
Introduction
181
Applying the recipe to nonclassical logics
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
Bibliography
1774
Index
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
Index
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
A Links to Saturation Based Provers
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
HANDBOOK OF AUTOMATED REASONING
2109
Concept index
2115
Copyright

Common terms and phrases

About the author (2001)

David Robinson is Lecturer in Marketing at the University of California, Berkeley, and has taught at Stanford, University of San Francisco, and Santa Clara University. He studied at the University of Durham in England and then at Oxford. His Ph.D. in Psychology is from Brown University in Rhode Island and his MBA is from the Unversity of North Carolina, Chapel Hill. Every year more that 1,000 students take his Principles of Business class, and running the class is a good opportunity for him to practice his interest in service operations. Each summer, Dr. Robinson takes students on a Travel Study to the People's Republic of China. Observing intercultural differences in behavior led him to write about American practices that people take for granted.

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

Bibliographic information