Visualizing and Animating Proofs in the Mathematical Foundations of Computer Science

对于许多计算机科学本科生来说，证明定理并不有趣，因为它通常涉及数学记数，纸笔工作环境，而且没有立即的反馈。在自动机理论课程中，定理是理解语言、自动机和语法之间关系的一大部分，然而本科生对这些定理的许多证明只有一个肤浅的理解。我们将开发教学软件来帮助理解特定的定理，即那些证明将一种形式转换为另一种形式的定理。例如，将上下文无关文法(CFG)的定义转换为等价下推自动机(PDA)的定义。为了帮助理解这一证明，我们的软件将允许用户输入CFG，并通过几个步骤将其转换为等效的PDA。我们已经设计了几个交互式和可视化的软件工具，允许学生试验语法和自动机，并收到即时反馈。例如，使用我们的工具包，学生可以构建和测试自动机、下推自动机和图灵机的非确定性版本。我们开发的新工具将具有类似于我们现有工具的界面，例如上面构建的PDA将类似于襟翼中的PDA。工具将在夏季开发，并集成到自动机理论课程中。开发的所有工具和课程材料将通过匿名ftp提供给其他人使用。

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.