# Handbook of Automated Reasoning, 第 2 巻 (Google eブックス)

Alan J.A. Robinson, Andrei Voronkov
Elsevier, 2001/06/22 - 2128 ページ
Handbook of Automated Reasoning

レビューが見つかりませんでした。

### 目次

 David McAllester and Christopher Lynch 21 FirstOrder Resolution Methods 89 HANDBOOK OF AUTOMATED REASONING 94 Introduction 103 Clause Tableaux 125 Tableaux as a Framework 152 Comparing Calculi 164 Historical Remarks Resources 167
 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 著作権