UID:
almahu_9947420900302882
Format:
1 online resource (1187 p.)
Edition:
1st edition
ISBN:
1-282-28494-0
,
9786612284946
,
0-08-053279-9
Content:
Handbook of Automated Reasoning
Note:
Description based upon print version of record.
,
Front Cover; Handbook of Automated Reasoning, Volume II; Copyright Page; Preface; Contents; Part V: Higher-order logic and logical frameworks; Chapter 15. Classical Type Theory; 1 Introduction to type theory; 2 Metatheoretical foundations; 3 Proof search; 4 Conclusion; Bibliography; Index; Chapter 16. Higher-Order Unification And Matching; 1 Type Theory and Other Set Theories; 2 Simply Typed ?-calculus; 3 Undecidability; 4 Huet's Algorithm; 5 Scopes Management; 6 Decidable Subcases; 7 Unification in ?-calculus with Dependent Types; Bibliography; Index; Chapter 17. Logical Frameworks
,
1 Introduction2 Abstract syntax; 3 Judgments and deductions; 4 Meta-programming and proof search; 5 Representing meta-theory; 6 Appendix: the simply-typed ?-calculus; 7 Appendix: the dependently typed ?-calculus; 8 Conclusion; Bibliography; Index; Chapter 18. Proof-Assistants Using Dependent Type Systems; 1 Proof checking; 2 Type-theoretic notions for proof checking; 3 Type systems for proof checking; 4 Proof-development in type systems; 5 Proof assistants; Bibliography; Index; Name index; Part VI: Nonclassical logics
,
Chapter 19. Nonmonotonic Reasoning: Towards Efficient Calculi And Implementations1 General Nonmonotonic Logics; 2 Automating General Nonmonotonic Logics; 3 From Automated Reasoning to Disjunctive Logic Programming; 4 Nonmonotonic Semantics of Logic Programs; 5 Implementing Nonmonotonic Semantics; 6 Benchmarks; 7 Conclusion; Bibliography; Index; Chapter 20. Automated Deduction For Many-Valued Logics; 1 Introduction; 2 What is a many-valued logic?; 3 Classification of proof systems for many-valued logics; 4 Signed logic: reasoning classically about finitely-valued logics; 5 Signed resolution
,
6 An example7 Optimization of transformation rules; 8 Remarks on infinitely-valued logics; Bibliography; Index; Chapter 21. Encoding Two-Valued Nonclassical Logics In Classical Logic; 1 Introduction; 2 Background; 3 Encoding consequence relations; 4 The standard relational translation; 5 The functionl translation; 6 The semi-functional translation; 7 Variations and alternatives; 8 Conclusion; Bibliography; Index; Chapter 22. Connections In Nonclassical Logics; 1 Introduction; 2 Prelude: Connections in classical first-order logic; 3 Labelled systems; 4 Propositional intuitionistic logic
,
5 First-order intuitionistic logic6 Normal modal logics up to S4; 7 The S5 family; Bibliography; Index; Part VII: Decidable classes and model building; Chapter 23. Reasoning In Expressive Description Logics; 1 Introduction; 2 Description Logics; 3 Description Logics and Propositional Dynamic Logics; 4 Unrestricted Model Reasoning; 5 Finite Model Reasoning; 6 Beyond Basic Description Logics; 7 Conclusions; Bibliography; Index; Chapter 24.Model Checking; 1 Introduction; 2 Logical Languages, Expressiveness; 3 Second Order Languages; 4 Model Transformations and Properties
,
5 Equivalence reductions
,
English
Additional Edition:
ISBN 0-444-50813-9
Language:
English
Bookmarklink
