Accession Number : AD0804036

Title :   A COMPUTER PROGRAM FOR DISCOVERING AND PROVING SEQUENTIAL RECOGNITION RULES FOR WELL-FORMED FORMULAS DEFINED BY A BACKUS NORMAL FORM GRAMMAR.

Descriptive Note : Final rept.,

Corporate Author : CARNEGIE INST OF TECH PITTSBURGH PA

Personal Author(s) : London, Ralph L.

Report Date : MAY 1964

Pagination or Media Count : 93

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)

Descriptors :   *COMPUTER PROGRAMS), (*PROGRAMMING LANGUAGES, ARTIFICIAL INTELLIGENCE, LANGUAGE, THESES, SYNTAX, CHARACTER RECOGNITION, GRAMMARS, MATHEMATICAL LOGIC, THEOREMS, MACHINE TRANSLATION.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE