A COMPUTER PROGRAM FOR DISCOVERING AND PROVING SEQUENTIAL RECOGNITION RULES FOR WELL-FORMED FORMULAS DEFINED BY A BACKUS NORMAL FORM GRAMMAR.
Abstract
A report is presented based upon a computer program which will discover rules for the recognition of grammatical strings when given a simple Backus Normal Form grammar. The program attempts to prove that these rules are both necessary and sufficient to characterize grammatical strings. The main mathematical techniques that are mechanized are induction and case analysis. In addition the program is capable of producing counter-examples. Since the program is writing proofs, several (meta-)proofs are included asserting the correctness of the produced proofs. The program exists for two reasons. First, it will construct a recognizer for some Backus Normal Form grammars and provide a proof of the validity of the recognizer. Second, its domain is a convenient one for proving theorems by machines, especially those whose proofs may use fairly involved case analysis. The overall strategy used to discover the rules and to prove them valid is described, followed by a discussion of the program organization and internal representations. Limitations and possible improvements to the present program are mentioned. An assessment is made of the mathematical accomplishments of the program and the value of the program as a mathematical aid. An appendix presents the output of four examples of program runs. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1964
- Accession Number
- AD0804036
Entities
People
- Ralph L. London
Organizations
- Carnegie Institute of Technology