Handbook of Automated Reasoning, Volume 2

Front Cover
Elsevier, 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

REWRITING 535
999
SOLVING NUMERICAL CONSTRAINTS
1000
HIGHERORDER UNIFICATION AND MATCHING
1009
HigherOrder Unification and Matching
1011
Unification in Xcalculus with Dependent Types
1049
HANDBOOK OF AUTOMATED REASONING
1054
Index
1061
LOGICAL FRAMEWORKS
1063
Partial Order Techniques
1751
Bounded Model Checking
1755
Abstractions
1759
Compositionality and Modular Verification
1764
Further Topics
1767
Bibliography
1774
103
1775
Index
1788

Induction
1069
Alan Bundy
1087
THE INVERSE METHOD
1096
Name Index
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
AUTOMATED DEDUCTION FOR MANYVALUED LOGICS
1355
reasoning classically about finitelyvalued logics
1368
An example
1389
Classical Logic
1403
NORMAL FORM TRANSFORMATIONS
1428
INDUCTIONLESS INDUCTION
1478
COMPUTING SMALL CLAUSE NORMAL FORMS
1481
CONNECTIONS IN NONCLASSICAL LOGICS
1487
Labelled Systems
1516
Propositional intuitionistic logic
1528
Firstorder intuitionistic logic
1545
Normal modal logics up to S4
1553
The S5 family
1567
Decidable classes and model building
1579
Description Logics
1586
Description Logics and Propositional Dynamic Logics
1593
Finite Model Reasoning
1610
Beyond Basic Description Logics
1619
Conclusions
1626
MODEL CHECKING
1635
Logical Languages Expressiveness
1641
Second Order Languages
1654
Model Transformations and Properties
1670
Equivalence reductions
1681
Completeness
1689
Decision Procedures
1700
8
1711
Modelling of Reactive Systems
1724
Matthias Baaz Uwe Egly and Alexander Leitsch
1730
Symbolic Model Checking
1735
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
186
1845
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
HANDBOOK OF AUTOMATED REASONING
1959
209
1960
COMBINING SUPERPOSITION SORTS AND SPLITTING
1965
289
2009
Equality and other theories
2010
MODEL ELIMINATION AND CONNECTION
2015
306
2115
967
2117
503
2121
Copyright

Other editions - View all

Common terms and phrases

References to this book

All Book Search results »

About the author (2001)

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

Bibliographic information