Mathematical Reasoning: The History and Impact of the DReaM Group

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