Browse Prior Art Database

COMPUTATIONAL LOGIC: STRUCTURE SHARING AND PROOF OF PROGRAM PROPERTIES PART II

IP.com Disclosure Number: IPCOM000128899D
Original Publication Date: 1975-Apr-01
Included in the Prior Art Database: 2005-Sep-20
Document File: 12 page(s) / 45K

Publishing Venue

Software Patent Institute

Related People

Moore, J. Strothers: AUTHOR [+3]

Abstract

This paper describes a program which automatically proves a wide variety of theorems about functions written in a subset of pure LISP. Features of this program include: The program is fully automatic, requiring no information from the user except the LISP definitions of the functions involved and the statement of the theorem to be proved. No inductive assertions are required from the user. The program uses structural induction when required, automatically generating its own induction formulas. All relationships in the theorem are expressed in terms of user defined LISP functions, rather than a second logical language. The system employs no built-in information about any nonprimitive function. All properties required for any function involved in a proof are derived and established automatically. The program is capable of generalizing some theorems in order to prove them; in doing so, it often generates interesting lemmas. The program can write new, recursive LISP functions automatically in attempting to generalize a theorem. Finally, the program is very fast by theorem proving standards, requiring around 10 seconds per proof.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 10% of the total text.

Page 1 of 12

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

©; Xerox Palo Alto Research Center, April 1975

COMPUTATIONAL LOGIC: STRUCTURE SHARING AND PROOF OF PROGRAM PROPERTIES PART II

BY J STROTHER MOORE

CSL 75-2 APRIL 1975

This paper describes a program which automatically proves a wide variety of theorems about functions written in a subset of pure LISP. Features of this program include: The program is fully automatic, requiring no information from the user except the LISP definitions of the functions involved and the statement of the theorem to be proved. No inductive assertions are required from the user. The program uses structural induction when required, automatically generating its own induction formulas. All relationships in the theorem are expressed in terms of user defined LISP functions, rather than a second logical language. The system employs no built-in information about any nonprimitive function. All properties required for any function involved in a proof are derived and established automatically. The program is capable of generalizing some theorems in order to prove them; in doing so, it often generates interesting lemmas. The program can write new, recursive LISP functions automatically in attempting to generalize a theorem. Finally, the program is very fast by theorem proving standards, requiring around 10 seconds per proof.

Key Words and Phrases: LISP, automatic theorem-proving, structural induction, program verification
CR Categories: 3.64, 4.22, 5.21
XEROX
PALO ALTO RESEARCH CENTER 3333 COYOTE HILL ROAD/PALO ALTO/CALIFORNIA 94304

TABLE OF CONTENTS

ABSTRACT

TABLE OF CONTENTS ..... II
PREFACE ..... IV
ACKNOWLEDGMENTS ..... V
INTRODUCTION TO PART II ..... 77
CHAPTER 1 FOUNDATIONS ..... 85

1.1 The Theory of Lists ..... 85
1.2 LISP and the Theory of Lists ..... 93
CHAPTER 2 PROVING THEOREMS IN THE THEORY ..... 96 2.1 Evaluation, Recursion, and Induction ..... 96
2.2 An Example of Evaluation and Induction ..... 99
2.3 An Example of Additional Techniques ..... 101
CHAPTER 3 DESCRIPTION OF THE THEOREM PROVER ..... 104

3.1 Overview and Control Structure ..... 104
3.2 Evaluation ..... 109
3.3 Normalization ..... 122
3.4 Reduction ..... 129
3.5 Simplification ..... 133
3.6 Fertilization ..... 135

Xerox Corporation Page 1 Apr 01, 1975

Page 2 of 12

COMPUTATIONAL LOGIC: STRUCTURE SHARING AND PROOF OF PROGRAM PROPERTIES PART II

3.7 Generalization and Type Functions ..... 144
3.8 Induction ..... 159
3.9 Technical Information ..... 171
CHAPTER 4 DETAILED EXAMPLES OF PROGRAM OUTPUT ..... 173

4.1 Introduction to the Examples ..... 173
4.2 Sample Output 1 ..... 174
4.3 Sample Output 2 ..... 177
4.4 Sample Output 3 ..... 181
4.5 Sample Output 4 ..... 186
CHAPTER 5 EXTENSIONS ..... 191

5.1 Termination ..... 191
5.2 Iteration ..... 194
CHAPTER 6 CONCLUSIONS ..... 200

6.1 Built-in Information ..... 200
6.2 Automatic Generation of Natural Lemmas ..... 203
6.3 Design Philosophy of the Program ..... 205
APPENDIX A FUNCTION DEFINITION...