Handbook of automated reasoning
Handbook of Automated Reasoning
| Otros Autores: | , |
|---|---|
| Formato: | Libro electrónico |
| Idioma: | Inglés |
| Publicado: |
Amsterdam ; London :
Elsevier
c2001.
|
| Edición: | 1st edition |
| Materias: | |
| Ver en Biblioteca Universitat Ramon Llull: | https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009627158506719 |
Tabla de Contenidos:
- 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
