Handbook of automated reasoning / editors, Alan Robinson and Andrei Voronkov.

Format:

Book

Contributor:

Robinson, J. A. (John Alan)

Voronkov, A. (Andrei), 1959-

Language:

English

Subjects (All):

Qualitative reasoning.

Artificial intelligence.

Physical Description:

1 online resource (1187 p.)

Edition:

1st edition

Place of Publication:

Amsterdam ; London : Elsevier, c2001.

Language Note:

English

System Details:

text file

Summary:

Handbook of Automated Reasoning

Contents:

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

Notes:

Description based upon print version of record.

Includes bibliographical references and indexes.

ISBN:

9786612284946

9781282284944

1282284940

9780080532790

0080532799

OCLC:

609843470