Title: 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.