ebook img

The Computer Modelling of Mathematical Reasoning Alan Bundy PDF

339 Pages·2010·4.17 MB·English
by  
Save to my drive
Quick download
Download
Most books are stored in the elastic cloud where traffic is expensive. For this reason, we have a limit on daily download.

Preview The Computer Modelling of Mathematical Reasoning Alan Bundy

The Computer Modelling of Mathematical Reasoning Alan Bundy This digital edition is based on the fourth printing (1986 and 1990) with corrections. It also incorporates the errata from the author’s website (compiled by Helen Lowe in April 1997). Edited for online publication by Tobias Edler von Koch. This digital edition Copyright (cid:13)c 2010 by Alan Bundy. All rights reserved. Preface This book started as notes for a postgraduate course in Mathematical Rea- soning given in the Department of Artificial Intelligence at Edinburgh from 1979 onwards. Students on the course are drawn from a wide range of back- grounds: Psychology, Computer Science, Mathematics, Education, etc. The first draft of the notes was written during a terms sabbatical leave in 1980. Later they were used for a similar course at undergraduate level. While there are now several textbooks on Artificial Intelligence tech- niques and, more particularly, on Problem Solving and Theorem Proving, I felt the need for a book concentrating on applications of these techniques to Mathematics. There was certainly enough material, but it was scattered in research journals, conference proceedings and theses. If it were collected together I hoped it might prove of interest to a wider audience than the usual artificial intelligentsia; I hoped that mathematicians and educational- ists might find it a eye opener to how computational ideas could shed light on the process of doing Mathematics. I also hoped to give more unity to some, rather disparate, pieces of re- search. In particular, I wanted to show how the, so called, ‘non-Resolution theorem proving’ techniques could be readily brought into a Resolution framework, and how this helped us to relate the various techniques – cre- ating coherence from confusion. In order to achieve this goal I have taken stronghistoricallibertiesinmydescriptionsoftheworkofBoyerandMoore, Gelernter, Lenat, etc. Ihaveredescribedtheirworkinauniformframework, ignoring aspects of peripheral interest, and focussing on what I take to be their essential contribution. I call such descriptions, rational reconstruc- tions. This does not imply that the original work was irrational – only that my reconstructions are rational. I apologise to any of the rationally recon- structed who feel mistreated. My excuse is that the reworking of research into a coherent whole is a vital, but neglected, part of Artificial Intelligence research, and that it is better to have tried and failed than never to have tried at all. i ii Preface Reading Strategies It is not necessary to be a professional mathematician or computer scien- tist to read this book, but the book does presuppose some mathematical knowledge. For instance, it is necessary to know what a set and a group are. I have endeavoured to make it fairly self contained, e.g. by including an introduction to mathematical logic. But self-containedness brings its own problems; if the book is not to be too long, then the pace must not be too slow. I have tried to get the reader quickly to the heart of the book – the techniques of automatic inference – without losing him on the way. • Chapter 1 is a general introduction; it motivates the subject and gives some of the historical background. • Part I is a three chapter introduction to Mathematical Logic; it de- scribes only those aspects of logic that are required to understand the rest of the book, and may be omitted by anyone who understands elementary predicate logic. • Part II is a three chapter introduction to Resolution theorem proving. It may be omitted by anyone who knows what SL Resolution is. • Part III consists of five rational reconstructions of theorem proving techniques or programs. Each was selected because it contributes an important partial solution to the problem of guiding the search for a proof. This part is the heart of the book. • Part IV is a two chapter discussion of aspects of mathematical rea- soning other than proving theorems – although they both reduce to theorem proving in the end. • Part V is a three chapter investigation of the more mathematical as- pects of theorem proving, e.g. completeness proofs. It may have to be omitted by those without a good background in Mathematics. • The last chapter discusses some applications of the techniques de- scribed in the book, from algebraic manipulation to education. • The appendices include: computer programs, notational discussions and solutions to exercises. Scattered throughout the book are exercises of an elementary nature. Readers may want to use these to test their understanding of the text. Some of the exercises contain material that is drawn on later in the book. Solutions may be found in appendix D. Preface iii Readers already familiar with the literature of mathematical reasoning may be particularly interested in the non-standard presentations of Gelern- ter’s Geometry Machine, in chapter 10, and Lenat’s AM, in chapter 13. Section 10.5 onwards, of chapter 10, contains new results. Acknowledgements I would like to thank: Gordon Plotkin, who was an untiring source of in- formation; Richard O’Keefe, Leon Sterling, Alan Borning, David Plummer, Roy Dyckhoff, Lincoln Wallen and Alberto Pettorossi, who helped me de- bug the drafts; Bob Boyer, J Moore, Gerard Huet, Woody Bledsoe, Robert ShostakandDougLenat,whokindlyreadthechaptersdescribingtheirwork and gave me invaluable feedback; Alan Black, Mike Howry, Bill Clocksin, Jane Hesketh and Keh. Jiann Chen for giving feedback on the first edition of the book; and Liam Lynch and Roberto Desimone for assisting with the second edition. The students of the Department of Artificial Intelligence at Edinburgh were involuntary guinea pigs. iv Preface Contents 1 Introduction 1 1.1 Why read this book? . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 What good is Automatic Mathematical Reasoning . . . . . . 2 1.3 The Historical Perspective . . . . . . . . . . . . . . . . . . . . 3 1.3.1 Mathematical Logic . . . . . . . . . . . . . . . . . . . 3 1.3.2 Psychological Studies . . . . . . . . . . . . . . . . . . 5 1.3.3 Automatic Theorem Proving . . . . . . . . . . . . . . 7 1.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 I Formal Notation 11 2 Arguments about Propositions 13 2.1 Truth Functional Connectives . . . . . . . . . . . . . . . . . . 14 2.1.1 Negation . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.1.2 Conjunction . . . . . . . . . . . . . . . . . . . . . . . . 14 2.1.3 Disjunction . . . . . . . . . . . . . . . . . . . . . . . . 15 2.1.4 Implication . . . . . . . . . . . . . . . . . . . . . . . . 16 2.1.5 Double Implication . . . . . . . . . . . . . . . . . . . . 17 2.2 Propositional Formulae . . . . . . . . . . . . . . . . . . . . . 18 2.2.1 Semantic Trees . . . . . . . . . . . . . . . . . . . . . . 19 2.2.2 Equivalences . . . . . . . . . . . . . . . . . . . . . . . 21 2.2.3 Tautologies and Contradictions . . . . . . . . . . . . . 22 2.2.4 Identifying Correct Arguments - Part 1 . . . . . . . . 23 2.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3 The Internal Structure of Propositions 25 3.1 Functions and Predicates: Variables and Constants . . . . . . 25 3.2 The Status of Variables . . . . . . . . . . . . . . . . . . . . . 28 3.3 The Meaning of Formulae . . . . . . . . . . . . . . . . . . . . 31 3.3.1 Interpretations . . . . . . . . . . . . . . . . . . . . . . 32 3.3.2 Interpreting Formulae . . . . . . . . . . . . . . . . . . 33 3.3.3 Some Definitions . . . . . . . . . . . . . . . . . . . . . 34 v vi Preface 3.4 Identifying Correct Arguments - Part 2 . . . . . . . . . . . . 35 3.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 4 Miscellaneous Topics 39 4.1 Higher Order Logics . . . . . . . . . . . . . . . . . . . . . . . 39 4.1.1 Variable Functions and Predicates . . . . . . . . . . . 39 4.1.2 Functionals . . . . . . . . . . . . . . . . . . . . . . . . 40 4.1.3 Lambda Abstraction . . . . . . . . . . . . . . . . . . . 41 4.1.4 Omega Order Logic . . . . . . . . . . . . . . . . . . . 41 4.2 Mathematical Theories . . . . . . . . . . . . . . . . . . . . . . 42 4.2.1 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . 42 4.2.2 Group Theory . . . . . . . . . . . . . . . . . . . . . . 43 4.2.3 Natural Number Arithmetic . . . . . . . . . . . . . . . 44 4.3 Some Practical Hints . . . . . . . . . . . . . . . . . . . . . . . 46 4.3.1 Function or Predicate? . . . . . . . . . . . . . . . . . . 47 4.3.2 An Advantage of Avoiding Functions . . . . . . . . . . 47 4.3.3 Variadic Functions and Predicates . . . . . . . . . . . 48 4.3.4 Representing Negation . . . . . . . . . . . . . . . . . . 49 4.3.5 The Importance of a Semantics . . . . . . . . . . . . . 50 4.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 II Uniform Proof Procedures 53 5 Formalizing the Notion of Proof 55 5.1 The Resolution Rule . . . . . . . . . . . . . . . . . . . . . . . 57 5.1.1 Stage 1 – Variable Free Resolution . . . . . . . . . . . 57 5.1.2 Stage 2 – Binary Resolution . . . . . . . . . . . . . . . 58 5.1.3 Stage 3 – Full Resolution . . . . . . . . . . . . . . . . 59 5.1.4 Factoring . . . . . . . . . . . . . . . . . . . . . . . . . 60 5.2 Kowalski Form . . . . . . . . . . . . . . . . . . . . . . . . . . 60 5.3 The Paramodulation Rule . . . . . . . . . . . . . . . . . . . . 62 5.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 6 Searching for a Refutation 65 6.1 Following Your Nose . . . . . . . . . . . . . . . . . . . . . . . 67 6.2 Representing Choice . . . . . . . . . . . . . . . . . . . . . . . 68 6.3 AND choices and OR choices . . . . . . . . . . . . . . . . . . 69 6.4 Preventing Looping . . . . . . . . . . . . . . . . . . . . . . . . 71 6.5 Choosing Where to Start . . . . . . . . . . . . . . . . . . . . 72 6.6 Non-Horn Clauses, Case Analysis and Ancestor Resolution. . 73 6.7 How to Make OR Choices . . . . . . . . . . . . . . . . . . . . 76 6.7.1 Depth First Search . . . . . . . . . . . . . . . . . . . . 76 6.7.2 Breadth First Search . . . . . . . . . . . . . . . . . . . 77 Preface vii 6.7.3 Heuristic Search . . . . . . . . . . . . . . . . . . . . . 78 6.8 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 7 Criticisms of Uniform Proof Procedures 81 7.1 The Contribution of Logic . . . . . . . . . . . . . . . . . . . . 82 7.2 A Resolution Proof and the Combinatorial Explosion . . . . . 83 7.3 Attempts to Guide Search . . . . . . . . . . . . . . . . . . . . 85 7.3.1 Paramodulation . . . . . . . . . . . . . . . . . . . . . 85 7.3.2 Cheating Techniques . . . . . . . . . . . . . . . . . . . 86 7.4 Analysing Human Proofs . . . . . . . . . . . . . . . . . . . . 87 7.5 Alternative Axiomatization . . . . . . . . . . . . . . . . . . . 89 7.6 A New Methodology . . . . . . . . . . . . . . . . . . . . . . . 91 7.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 III Guiding Search 95 8 Decision Procedures for Inequalities 97 8.1 Axioms for Inequalities . . . . . . . . . . . . . . . . . . . . . . 97 8.2 Some Human Proofs . . . . . . . . . . . . . . . . . . . . . . . 99 8.3 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 8.4 The Sup-Inf Method . . . . . . . . . . . . . . . . . . . . . . . 101 8.4.1 Bledsoe Real Arithmetic . . . . . . . . . . . . . . . . . 101 8.4.2 An Overview of the Method . . . . . . . . . . . . . . . 101 8.4.3 Assigning Types to Skolem Constants . . . . . . . . . 103 8.5 Variable Elimination . . . . . . . . . . . . . . . . . . . . . . . 108 8.5.1 An Overview of the Extended Procedure . . . . . . . . 109 8.5.2 Elimination of Variables using Interpolation . . . . . . 111 8.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 9 Rewrite Rules 113 9.1 What are Rewrite Rules? . . . . . . . . . . . . . . . . . . . . 114 9.2 Some Sample Rewrite Rule Sets . . . . . . . . . . . . . . . . . 115 9.2.1 Literal Normal Form . . . . . . . . . . . . . . . . . . . 115 9.2.2 Algebraic Simplification . . . . . . . . . . . . . . . . . 116 9.2.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . 117 9.3 Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 9.4 Other Important Properties . . . . . . . . . . . . . . . . . . . 119 9.5 Applying Rewrite Rules . . . . . . . . . . . . . . . . . . . . . 119 9.5.1 Inside Out Application . . . . . . . . . . . . . . . . . . 120 9.5.2 Outside In Application . . . . . . . . . . . . . . . . . . 120 9.6 Proving Rules Canonical and Church-Rosser . . . . . . . . . . 122 9.6.1 Local Confluence . . . . . . . . . . . . . . . . . . . . . 124 9.6.2 Critical Pairs . . . . . . . . . . . . . . . . . . . . . . . 125 viii Preface 9.6.3 Improving Non-Confluent Rule Sets . . . . . . . . . . 129 9.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 10 Using Semantic Information to Guide Proofs 131 10.1 Formalising Geometry . . . . . . . . . . . . . . . . . . . . . . 132 10.2 Geometric Proofs . . . . . . . . . . . . . . . . . . . . . . . . . 134 10.3 Constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . 135 10.4 What is the Diagram? . . . . . . . . . . . . . . . . . . . . . . 138 10.5 Can the Diagram be Generalized? . . . . . . . . . . . . . . . 141 10.6 The Trouble with Non-Horn Clauses . . . . . . . . . . . . . . 143 10.7 The Theoretical Underpinning for Semantic Checking . . . . 145 10.8 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 11 The Productive Use of Failure 149 11.1 The Formal Theory of LISP . . . . . . . . . . . . . . . . . . . 150 11.2 Symbolic Evaluation . . . . . . . . . . . . . . . . . . . . . . . 152 11.3 The Method of Induction . . . . . . . . . . . . . . . . . . . . 154 11.4 Generalizing the Theorem to be Proved . . . . . . . . . . . . 157 11.5 Applications to Arithmetic . . . . . . . . . . . . . . . . . . . 159 11.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 12 Formalizing Control Information 163 12.1 Reading Between the Lines . . . . . . . . . . . . . . . . . . . 164 12.2 Equation Solving Methods . . . . . . . . . . . . . . . . . . . . 165 12.2.1 Isolation . . . . . . . . . . . . . . . . . . . . . . . . . . 166 12.2.2 Collection . . . . . . . . . . . . . . . . . . . . . . . . . 167 12.2.3 Attraction . . . . . . . . . . . . . . . . . . . . . . . . . 168 12.3 Reasoning About Problems and Methods . . . . . . . . . . . 170 12.3.1 Defining the Methods with Axioms . . . . . . . . . . . 170 12.3.2 Searching for a Solution . . . . . . . . . . . . . . . . . 172 12.3.3 Meta Level Reasoning . . . . . . . . . . . . . . . . . . 173 12.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174 IV Mathematical Invention 177 13 Concept Formation 179 13.1 How Definitions and Conjectures Can Be Made . . . . . . . . 180 13.2 Operations of Concept Formation . . . . . . . . . . . . . . . . 181 13.2.1 Creating New Concepts . . . . . . . . . . . . . . . . . 181 13.2.2 Finding Examples of Concepts . . . . . . . . . . . . . 182 13.2.3 Checking Examples of Concepts . . . . . . . . . . . . 182 13.2.4 Making Conjectures . . . . . . . . . . . . . . . . . . . 183 13.3 Formalizing the Knowledge . . . . . . . . . . . . . . . . . . . 183

Description:
This book started as notes for a postgraduate course in Mathematical Rea- soning given Readers already familiar with the literature of mathematical reasoning.
See more

The list of books you might like

Most books are stored in the elastic cloud where traffic is expensive. For this reason, we have a limit on daily download.