Gabbay / Siekmann / Woods Computational Logic

1. Auflage 2014
ISBN: 978-0-08-093067-1
Verlag: Elsevier Science & Techn.
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band Volume 9, 736 Seiten, Web PDF

Reihe: Handbook of the History of Logic

Handbook of the History of Logic brings to the development of logic the best in modern techniques of historical and interpretative scholarship. Computational logic was born in the twentieth century and evolved in close symbiosis with the advent of the first electronic computers and the growing importance of computer science, informatics and artificial intelligence. With more than ten thousand people working in research and development of logic and logic-related methods, with several dozen international conferences and several times as many workshops addressing the growing richness and diversity of the field, and with the foundational role and importance these methods now assume in mathematics, computer science, artificial intelligence, cognitive science, linguistics, law and many engineering fields where logic-related techniques are used inter alia to state and settle correctness issues, the field has diversified in ways that even the pure logicians working in the early decades of the twentieth century could have hardly anticipated. Logical calculi, which capture an important aspect of human thought, are now amenable to investigation with mathematical rigour and computational support and fertilized the early dreams of mechanised reasoning: 'Calculemus. The Dartmouth Conference in 1956 - generally considered as the birthplace of artificial intelligence - raised explicitly the hopes for the new possibilities that the advent of electronic computing machinery offered: logical statements could now be executed on a machine with all the far-reaching consequences that ultimately led to logic programming, deduction systems for mathematics and engineering, logical design and verification of computer software and hardware, deductive databases and software synthesis as well as logical techniques for analysis in the field of mechanical engineering. This volume covers some of the main subareas of computational logic and its applications. - Chapters by leading authorities in the field - Provides a forum where philosophers and scientists interact - Comprehensive reference source on the history of logic

Autoren/Hrsg.

Gabbay, Dov M.

Siekmann, Jörg H.

Woods, John

Inhaltsverzeichnis

1;Front Cover;1
2;Computational Logic ;4
3;Copyright ;5
4;Contents ;6
5;Editorial Note ;8
6;Contributors ;9
6.1;Authors;9
6.2;Readers;12
7;Part I: Introduction ;14
7.1;Chapter 1: Computational Logic ;16
7.1.1;Acknowledgements ;30
7.1.2;Bibliography ;30
7.2;Chapter 2: Logic and the Development of the Computer ;32
7.2.1;Bibliography ;37
8;Part II: General ;40
8.1;Chapter 3: What is a Logical System? An Evolutionary View: 1964–2014 ;42
8.1.1;1 Introduction ;42
8.1.2;2 Logical Systems as Consequence Relations ;45
8.1.3;3 Logical Systems as Algorithmic Proof Systems ;48
8.1.4;4 Logical Systems as Algorithmic Structured Consequence Relations ;50
8.1.5;5 Algorithmic Approximations of Logical Systems ;52
8.1.6;6 Logical Systems as Labelled Deductive Systems ;53
8.1.7;7 Aggregated Systems ;60
8.1.8;8 Practical Reasoning Systems ;62
8.1.9;9 New Notions of Logical Consequence ;72
8.1.10;10 Example: A TAR-logic ;75
8.1.11;11 Semantical Interpretation ;81
8.1.12;12 Discussion 1999 ;84
8.1.13;13 Modes of Evaluation ;85
8.1.14;14 The Reactive Paradigm in General ;87
8.1.15;15 Reactive Proof Theory ;98
8.1.16;16 Equational Approach to Logic ;101
8.1.17;17 Non-Deterministic Semantics for Logical Systems and the Equational Approach ;109
8.1.18;18 Input Output Logics ;112
8.1.19;19 Argumentation Networks as Logics ;113
8.1.20;20 Semantics ;122
8.1.21;21 Concluding Discussion 2014 ;126
8.1.22;Acknowledgements ;129
8.1.23;Bibliography ;129
9;Part III: Automated Reasoning ;134
9.1;Chapter 4: History of Interactive Theorem Proving ;136
9.1.1;1 Introduction ;136
9.1.2;2 Automath and Successors ;140
9.1.3;3 LCF and Successors ;148
9.1.4;4 Mizar ;157
9.1.5;5 Systems Based on Powerful Automation ;164
9.1.6;6 Research Topics in Interactive Theorem Proving ;169
9.1.7;Acknowledgements ;197
9.1.8;Bibliography ;197
9.2;Chapter 5: Automation of Higher-Order Logic ;216
9.2.1;1 Introduction ;216
9.2.2;2 Formalization of Quantificational Logic ;218
9.2.3;3 Church’s Simple Theory of Types (Classical Higher-Order Logic) ;222
9.2.4;4 Meta-Theory ;230
9.2.5;5 Skolemization and Unification ;234
9.2.6;6 Challenges for Automation ;239
9.2.7;7 Automated Theorem Provers ;242
9.2.8;8 Conclusion ;248
9.2.9;Acknowledgments ;248
9.2.10;Bibliography ;248
9.3;Chapter 6: Equational Logic and Rewriting ;256
9.3.1;1 Introduction ;256
9.3.2;2 Equational Logics and their Models ;258
9.3.3;3 Rewriting Techniques ;261
9.3.4;4 Rewriting and/for Equality in Theorem Proving ;266
9.3.5;5 Universal Power of Rewriting ;270
9.3.6;6 Conclusion ;275
9.3.7;Bibliography ;276
9.4;Chapter 7: Possibilistic Logic — An Overview ;284
9.4.1;1 Introduction ;284
9.4.2;2 Qualitative Possibility Theory - A Refresher ;286
9.4.3;3 Necessity-Based Possibilistic Logic and Related Issues ;294
9.4.4;4 Applications of Basic Possibilistic Logic ;308
9.4.5;5 Extensions of Possibilistic Logic ;318
9.4.6;6 Conclusion ;329
9.4.7;Acknowlegments ;330
9.4.8;Bibliography ;330
9.5;Chapter 8: Computerising Mathematical Text ;344
9.5.1;1 Background and Motivation ;344
9.5.2;2 Introduction ;350
9.5.3;3 The Goals of Mathlang and MPL;352
9.5.4;4 An Overview of Mathlang ;354
9.5.5;5 Connecting Mathlang to Formal Foundations ;370
9.5.6;6 Connecting MPL to Formal Foundation ;378
9.5.7;7 A Full Formalisation in COQ Via Mathlang: Chapter 1 of Landau’s “Grundlagen Der Analysis” ;384
9.5.8;8 Conclusion ;392
9.5.9;Bibliography ;393
10;Part IV: Computer Science ;398
10.1;Chapter 9: Concurrency Theory: A Historical Perspective on Coinduction and Process Calculi ;400
10.1.1;1 Introduction ;400
10.1.2;2 Concurrency ;401
10.1.3;3 Bisimulation and Coinduction ;403
10.1.4;4 Process Calculi ;423
10.1.5;5 Conclusion ;435
10.1.6;Acknowledgements ;436
10.1.7;Bibliography ;436
10.2;Chapter 10: Degrees of Unsolvability ;444
10.2.1;1 Introduction ;444
10.2.2;2 From Problems to Degrees ;446
10.2.3;3 Origins of Degree Theory ;448
10.2.4;4 Solution to Post’s Problem: The Priority Method ;454
10.2.5;5 From Finite to Infinite Injury ;458
10.2.6;6 Programmatic Papers and Books ;463
10.2.7;7 Global Questions About the Degree Structure D ;468
10.2.8;8 Basic Algebraic Properties of R ;472
10.2.9;9 The 0''' Priority Method;476
10.2.10;10 Global Questions About the Structure R ;477
10.2.11;11 Definability and Automorphisms ;480
10.2.12;12 Conclusion ;485
10.2.13;Acknowledgements ;486
10.2.14;Bibliography ;487
10.3;Chapter 11: Computational Complexity ;496
10.3.1;1 Introduction ;496
10.3.2;2 Early History ;497
10.3.3;3 NP-Completeness ;499
10.3.4;4 Structural Complexity ;501
10.3.5;5 Counting Classes ;505
10.3.6;6 Probabilistic Complexity ;505
10.3.7;7 Descriptive Complexity ;509
10.3.8;8 Finite Models ;510
10.3.9;9 Quantum Computing ;513
10.3.10;10 Future Directions ;514
10.3.11;11 Further Reading ;515
10.3.12;Acknowledgments ;516
10.3.13;Bibliography ;516
10.4;Chapter 12: Logic Programming ;524
10.4.1;1 Introduction ;524
10.4.2;2 The Historical Background ;528
10.4.3;3 The Procedural Interpretation of Horn Clauses ;535
10.4.4;4 The Semantics of Horn Clause Programs ;540
10.4.5;5 Negation as Failure — Part 1 ;545
10.4.6;6 Negation as Failure — Part 2 ;549
10.4.7;7 Abductive Logic Programming ;557
10.4.8;8 Constraint Logic Programming ;560
10.4.9;9 Argumentation ;561
10.4.10;10 Conclusions ;563
10.4.11;Acknowledgements ;564
10.4.12;Bibliography ;564
10.5;Chapter 13: Logic and Databases: A History of Deductive Databases ;572
10.5.1;1 Introduction ;572
10.5.2;2 Background ;575
10.5.3;3 Historical Background of Deductive Databases ;580
10.5.4;4 Theoretical Foundations of Deductive Databases ;584
10.5.5;5 Theory of Disjunctive Deductive Databases ;602
10.5.6;6 Systems, Companies and Applications ;607
10.5.7;7 Future Extensions Needed ;611
10.5.8;Acknowledgements ;616
10.5.9;Abbreviations ;617
10.5.10;Bibliography ;617
10.6;Chapter 14: Logics for Intelligent Agents and Multi-Agent Systems ;630
10.6.1;1 Introduction ;630
10.6.2;2 Modal Logic ;630
10.6.3;3 Specifying Single Agent’s Attitudes: BDI Logics ;633
10.6.4;4 Logics for Multi-Agent Systems ;641
10.6.5;5 Related Work ;651
10.6.6;6 Conclusion ;653
10.6.7;Acknowledgements ;654
10.6.8;Bibliography ;654
10.7;Chapter 15: Description Logics ;660
10.7.1;1 Introduction ;660
10.7.2;2 Historic Roots ;661
10.7.3;3 Syntax and Semantics ;663
10.7.4;4 Algorithmic Aspects ;667
10.7.5;5 Recent Developments ;669
10.7.6;6 Conclusions ;671
10.7.7;Acknowledgements ;671
10.7.8;Bibliography ;671
10.8;Chapter 16: Logics for the Semantic Web ;680
10.8.1;1 Introduction ;680
10.8.2;2 RDF and RDF Schema ;681
10.8.3;3 Daml/Oil and Owl ;692
10.8.4;4 Rules ;697
10.8.5;5 Particular Challenges to Using Logic-based Knowledge Representation on the Web ;699
10.8.6;6 Recent Developments ;701
10.8.7;Acknowledgements ;703
10.8.8;Bibliography ;703
11;Index ;712