Discoveries and experiments in the automation of mathematical reasoning
Benjamin Shults, Larry M. Hines, Robert S. Boyer · 1997
vii List of Figures xii Chapter 1. Introduction 1 1.1 Reasoning in Mathematics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.1.1 Reasoning with Knowledge . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.1.2 Higher-Order Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2 Interface Issues . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.2.1 Output . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.2.2 Input . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.3 Interaction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.3 A Survey of the Automation of Reasoning . . . . . . . . . . . . . . . . . . . . . . . 8 1.4 An Overview of the Dissertation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Chapter 2. Formal Reasoning 18 2.1 Language for a Theory . . . . . . . . . . . . . . . . . . . . . . . . . ....