A computer program for discovering and proving recognition rules for Backus Normal Form grammars

ABSTRACT

This paper is based upon a running computer program which will discover rules for the recognition of grammatical strings when given a simple Backus Normal Form (BNF) grammar [10]. 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. There are two reasons for writing this program. First, we are interested in constructing efficient recognizers for simple BNF grammars. Second, the task of proving that a proposed recognizer is indeed a recognizer is sufficiently complex and difficult to make it a convenient area for proving theorems by machines, especially theorems whose proofs may use fairly involved case analysis.

REFERENCES

• 1: Brown, Peter J. A program to prove theorems by induction. Private communication, May 1963.
• 2: Carr, John W., III. Recent trends in computer programming and numerical analysis, in Applications of Digital Computers, edited by Walter F. Freiberger and William Prager. Ginn and Company, Boston, 1963, pp. 33-41.
• 3: Chomsky, N. Context free grammars and pushdown storage. Quarterly Progress Report No. 65, Research Laboratory of Electronics, Massachusetts Institute of Technology (Apr. 15, 1962), 187 - 194.
• 4: Evans, Arthur, Jr. An ALGOL-60 compiler. Paper presented at the 18th Annual Meeting of the Association for Computing Machinery, Denver, Colorado, Aug. 27, 1963.
• 5: Feldman, Jerome. A formal semantics for computer-oriented languages. Ph. D. thesis, Carnegie Institute of Technology, May, 1964.
• 6: Ingerman, Peter Zilahy. A translation technique for languages whose syntax is expressible in extended Backus normal form. Paper, Symposium of Symbolic Languages, Rome, 1962.
• 7: Lehmer, D. H. Automation and pure mathematics, in Applications of Digital Computers, edited by Walter F. Freiberger and William Prager. Ginn and Co., Boston, 1963, pp. 219 - 231.
• 8: Lehmer, D. H., et al. Machine proof of a theorem. Mathematics of Computation (Oct. 1962), 407 - 415.
• 9: London, Ralph L. A computer program for discovering and proving sequential recognition rules for well-formed formulas defined by a Backus normal form grammar. PhD. thesis, Carnegie Institute of Technology, May, 1964.
• 10: Peter Naur , J. W. Backus , F. L. Bauer , J. Green , C. Katz , J. McCarthy , A. J. Perlis , H. Rutishauser , K. Samelson , B. Vauquois , J. H. Wegstein , A. van Wijngaarden , M. Woodger, Report on the algorithmic language ALGOL 60, Communications of the ACM, v.3 n.5, p.299-314, May 1960 [doi>10.1145/367236.367262]
• 11: Newell, A., Shaw, J. C., and Simon, H. A. Report on a general problem-solving program. Proceedings of the International Conference on Information Processing, UNESCO (1959), 256 - 264.
• 12: Newell, Allen, et al. Information Processing Language-V Manual. Second edition. Prentice Hall Inc., Englewood Cliffs, N. J., 1964.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
          Subjects: Grammar types (e.g., context-free, context-sensitive)

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Mathematical induction

General Terms:
Theory