Mathematical Reasoning: The History and Impact of the DReaM Group

Description

This collection of essays examines  the key achievements and likely developments in the area of automated reasoning. In keeping with the group ethos, Automated Reasoning is interpreted liberally, spanning underpinning theory,  tools for reasoning, argumentation, explanation, computational creativity, and pedagogy. Wider applications including secure and trustworthy software,  and health care and emergency management.  The book starts with a technically oriented history of the Edinburgh Automated Reasoning Group, written by Alan Bundy, which is followed by chapters from leading researchers associated with the group.   Mathematical Reasoning: The History and Impact of the DReaM Group will  attract considerable interest from researchers and practitioners of Automated Reasoning, including postgraduates. It should also be of interest to those researching the history of AI.  Foreword AI, Automated Reasoning and Mathematics: DReaM Preface Overview Contents Acknowledgements Contents Contributors 1 The History of the DReaM Group 1.1 Why DReaM? 1.2 Arrival in Edinburgh 1.3 The Mecho Project 1.4 The Eco Project 1.5 Building a Wider Community 1.5.1 Rolling Funding and Platform Grants 1.5.2 Blue Book Notes and Trip Reports 1.5.3 International Collaboration 1.6 DReaM Motifs 1.6.1 Rigour and Heuristics 1.6.2 Meta-Level Reasoning 1.6.3 Why Prolog? 1.6.3.1 Meta-Level Axioms for Rippling 1.6.3.2 Meta-Level Axioms Attraction 1.6.4 The Productive Use of Failure 1.6.4.1 Suggesting Intermediate Lemmas 1.6.4.2 Lakatos Methods and Counter-Examples 1.6.4.3 Suggesting Changes of Representation 1.6.5 The Interaction of Multiple Reasoning Processes 1.6.5.1 Proof Planning: Abstraction of Deduction 1.6.6 Diverse Applications 1.6.6.1 Formal Methods 1.6.6.2 Cyber Security 1.6.6.3 Machine Learning of Proof Tactics 1.6.6.4 When Is a Theorem Interesting? 1.6.6.5 The Constructive Omega Rule, Induction and Diagrams 1.6.6.6 Category Theory and Analogy 1.6.6.7 Representing Uncertainty 1.7 Conclusion References 2 Recollections of Hope Park Square, 1970–1973 2.1 Arrival References 3 Adventures in Mathematical Reasoning 3.1 Introduction 3.2 Rippling 3.2.1 A Calculus for Rippling 3.2.2 Difference Matching and Unification 3.3 Proof Planning 3.3.1 Summing Series 3.3.2 A Divergence Critic 3.4 Mathematical Discovery 3.5 The Meta-Level 3.6 Conclusions References 4 Dynamic Proof Presentation 4.1 Introduction 4.1.1 Proof Presentation Style 4.1.2 Ongoing Issues 4.1.3 The Vision 4.1.4 Structure of Rest of Chapter 4.1.5 My DReaM Group Connections 4.2 A Running Example of a Procedural Proof 4.3 Focussing on Proof Steps in Procedural Proofs 4.4 Condensing Tactic-and-Subgoal Proof Trees 4.5 Expanding Proof Steps 4.6 Dynamic Presentation of Declarative Proofs 4.7 DReaM Group Contributions 4.7.1 Barnacle and XBarnacle 4.7.2 The Orthogonal Hierarchies of Method Trees 4.7.3 IsaPlanner 4.7.4 Hiproofs and Proof Refactoring 4.7.5 HipCam and Tactician 4.8 Technologies for Proof Presentation 4.9 Relationship Between Viewing and Editing Proofs 4.10 Further Related Work 4.11 Conclusions and Future Directions References 5 Proof Mechanization: From Dream to Reality 5.1 Prologue 5.2 Proof Planning 5.2.1 Nonstandard Analysis in λClam 5.2.2 IsaPlanner 5.2.2.1 Interlude: Graduation Time for IsaPlanner 5.3 Geometric Reasoning: Marrying Discovery and Proof 5.3.1 Of Chairs, Tables and Beer Mugs: Hilbert's Axiomatics 5.3.2 Geometric Discovery 5.3.2.1 Geometry Explorer 5.3.2.2 Hilbert's Implicit Reasoning and Idle-Time Proof Discovery 5.3.3 Computational Geometry 5.4 Conclusion 5.5 Epilogue References 6 Reasoned Modelling: Harnessing the Synergies Between Reasoning and Modelling 6.1 Introduction 6.2 Refinement-Based Development and Event-B 6.3 Reasoned Modelling Critics 6.4 Refinement Plans 6.5 Invariants Generation and HREMO 6.6 Design-Space Exploration 6.7 Future Work and Conclusion 6.7.1 Requirements, Domain Properties and Specifications 6.7.2 Hazard Analysis—What-if Style Scenarios 6.7.3 Enterprise Security Architecture 6.7.4 Conclusion Acknowledgements and Final Reflections References 7 Human-Like Computational Reasoning: Diagrams and Other Representations 7.1 The DReaM Research Environment 7.2 Diagrammatic Reasoning 7.3 Heterogeneous Reasoning 7.4 Accessible Diagrammatic Reasoning About Ontologies 7.5 How to Choose a Representation 7.6 Future Directions References 8 From Mathematical Reasoning to Crises in Different Languages: The Application of Failure-Driven Reasoning to Ontologies and Data 8.1 Introduction 8.2 Agents Reasoning About Their Ontologies 8.3 Into Ontology Matching: The Open Knowledge Project 8.4 Sharing Knowledge in Crises: Failure-Driven Query Rewriting 8.5 Multi-Lingual and Multi-Domain Matching 8.6 On to the Future References