Computational Logic (eBook)

Front Cover 1
Computational Logic 4
Copyright 5
Contents 6
Editorial Note 8
Contributors 9
Authors 9
Readers 12
Part I: Introduction 14
Chapter 1: Computational Logic 16
Acknowledgements 30
Bibliography 30
Chapter 2: Logic and the Development of the Computer 32
Bibliography 37
Part II: General 40
Chapter 3: What is a Logical System? An Evolutionary View: 1964–2014 42
1 Introduction 42
2 Logical Systems as Consequence Relations 45
3 Logical Systems as Algorithmic Proof Systems 48
4 Logical Systems as Algorithmic Structured Consequence Relations 50
5 Algorithmic Approximations of Logical Systems 52
6 Logical Systems as Labelled Deductive Systems 53
7 Aggregated Systems 60
8 Practical Reasoning Systems 62
9 New Notions of Logical Consequence 72
10 Example: A TAR-logic 75
11 Semantical Interpretation 81
12 Discussion 1999 84
13 Modes of Evaluation 85
14 The Reactive Paradigm in General 87
15 Reactive Proof Theory 98
16 Equational Approach to Logic 101
17 Non-Deterministic Semantics for Logical Systems and the Equational Approach 109
18 Input Output Logics 112
19 Argumentation Networks as Logics 113
20 Semantics 122
21 Concluding Discussion 2014 126
Acknowledgements 129
Bibliography 129
Part III: Automated Reasoning 134
Chapter 4: History of Interactive Theorem Proving 136
1 Introduction 136
2 Automath and Successors 140
3 LCF and Successors 148
4 Mizar 157
5 Systems Based on Powerful Automation 164
6 Research Topics in Interactive Theorem Proving 169
Acknowledgements 197
Bibliography 197
Chapter 5: Automation of Higher-Order Logic 216
1 Introduction 216
2 Formalization of Quantificational Logic 218
3 Church’s Simple Theory of Types (Classical Higher-Order Logic) 222
4 Meta-Theory 230
5 Skolemization and Unification 234
6 Challenges for Automation 239
7 Automated Theorem Provers 242
8 Conclusion 248
Acknowledgments 248
Bibliography 248
Chapter 6: Equational Logic and Rewriting 256
1 Introduction 256
2 Equational Logics and their Models 258
3 Rewriting Techniques 261
4 Rewriting and/for Equality in Theorem Proving 266
5 Universal Power of Rewriting 270
6 Conclusion 275
Bibliography 276
Chapter 7: Possibilistic Logic — An Overview 284
1 Introduction 284
2 Qualitative Possibility Theory - A Refresher 286
3 Necessity-Based Possibilistic Logic and Related Issues 294
4 Applications of Basic Possibilistic Logic 308
5 Extensions of Possibilistic Logic 318
6 Conclusion 329
Acknowlegments 330
Bibliography 330
Chapter 8: Computerising Mathematical Text 344
1 Background and Motivation 344
2 Introduction 350
3 The Goals of Mathlang and MPL 352
4 An Overview of Mathlang 354
5 Connecting Mathlang to Formal Foundations 370
6 Connecting MPL to Formal Foundation 378
7 A Full Formalisation in COQ Via Mathlang: Chapter 1 of Landau’s “Grundlagen Der Analysis” 384
8 Conclusion 392
Bibliography 393
Part IV: Computer Science 398
Chapter 9: Concurrency Theory: A Historical Perspective on Coinduction and Process Calculi 400
1 Introduction 400
2 Concurrency 401
3 Bisimulation and Coinduction 403
4 Process Calculi 423
5 Conclusion 435
Acknowledgements 436
Bibliography 436
Chapter 10: Degrees of Unsolvability 444
1 Introduction 444
2 From Problems to Degrees 446
3 Origins of Degree Theory 448
4 Solution to Post’s Problem: The Priority Method 454
5 From Finite to Infinite Injury 458
6 Programmatic Papers and Books 463
7 Global Questions About the Degree Structure D 468
8 Basic Algebraic Properties of R 472
9 The 0''' Priority Method 476
10 Global Questions About the Structure R 477
11 Definability and Automorphisms 480
12 Conclusion 485
Acknowledgements 486
Bibliography 487
Chapter 11: Computational Complexity 496
1 Introduction 496
2 Early History 497
3 NP-Completeness 499
4 Structural Complexity 501
5 Counting Classes 505
6 Probabilistic Complexity 505
7 Descriptive Complexity 509
8 Finite Models 510
9 Quantum Computing 513
10 Future Directions 514
11 Further Reading 515
Acknowledgments 516
Bibliography 516
Chapter 12: Logic Programming 524
1 Introduction 524
2 The Historical Background 528
3 The Procedural Interpretation of Horn Clauses 535
4 The Semantics of Horn Clause Programs 540
5 Negation as Failure — Part 1 545
6 Negation as Failure — Part 2 549
7 Abductive Logic Programming 557
8 Constraint Logic Programming 560
9 Argumentation 561
10 Conclusions 563
Acknowledgements 564
Bibliography 564
Chapter 13: Logic and Databases: A History of Deductive Databases 572
1 Introduction 572
2 Background 575
3 Historical Background of Deductive Databases 580
4 Theoretical Foundations of Deductive Databases 584
5 Theory of Disjunctive Deductive Databases 602
6 Systems, Companies and Applications 607
7 Future Extensions Needed 611
Acknowledgements 616
Abbreviations 617
Bibliography 617
Chapter 14: Logics for Intelligent Agents and Multi-Agent Systems 630
1 Introduction 630
2 Modal Logic 630
3 Specifying Single Agent’s Attitudes: BDI Logics 633
4 Logics for Multi-Agent Systems 641
5 Related Work 651
6 Conclusion 653
Acknowledgements 654
Bibliography 654
Chapter 15: Description Logics 660
1 Introduction 660
2 Historic Roots 661
3 Syntax and Semantics 663
4 Algorithmic Aspects 667
5 Recent Developments 669
6 Conclusions 671
Acknowledgements 671
Bibliography 671
Chapter 16: Logics for the Semantic Web 680
1 Introduction 680
2 RDF and RDF Schema 681
3 Daml/Oil and Owl 692
4 Rules 697
5 Particular Challenges to Using Logic-based Knowledge Representation on the Web 699
6 Recent Developments 701
Acknowledgements 703
Bibliography 703
Index 712