Visualizing and Animating Proofs in the Mathematical Foundations of Computer Science

点击翻译按钮获取中文摘要

Proving theorems is uninteresting to many computer science undergraduates as it usually involves mathematical notation, a pencil and paper working environment and no immediate feedback. In the automata theory course, theorems are a large part of understanding the relationships of languages, automata and grammars, yet undergraduates obtain only a superficial understanding of many of the proofs of these theorems. We will develop instructional software to aid in the understanding of specific theorems, namely those whose proofs convert one form to another form. For example, converting the definition of a context-free grammar (CFG) to the definition of an equivalent pushdown automaton (PDA). As an aid in understanding this proof, our software will allow the user to enter a CFG and convert it to the equivalent PDA through several steps. We have already designed several interactive and visual software tools that allow students to experiment with grammars and automata, receiving immediate feedback. For example, with our tool FLAP, students can build and test nondeterministic versions of automata, pushdown automata and Turing machines. The new tools we develop will have interfaces similar to our existing tools, for example the PDA constructed above will be similar to the PDA in FLAP. Tools will be developed during summers and integrated into the automata theory course. All tools and course materials developed will be made available via anonymous ftp for others to use.