论文标题
学期重写教育的工具
Tools in Term Rewriting for Education
论文作者
论文摘要
术语重写是Turing完整的计算模型。当教授计算机科学的学生时，将传达计算的关键特性以及在抽象层面分析程序的技术。本文迅速介绍了术语重写，并提供了几种自动工具来分析术语重写系统，这些系统是由Innsbruck大学计算逻辑组开发的。其中包括终止工具TTT2，Confluence Prover CSI，MKBTT和KBCV的完成工具，复杂性工具TCT，策略工具自动层以及Fort，Fort，为可确定的reprter Systems的一阶理论实施了决策程序。除了其在研究中的应用外，该软件池还证明对教学（例如，在国际暑期学校重写的多个版本中）也是无价的。
Term rewriting is a Turing complete model of computation. When taught to students of computer science, key properties of computation as well as techniques to analyze programs on an abstract level are conveyed. This paper gives a swift introduction to term rewriting and presents several automatic tools to analyze term rewrite systems which were developed by the Computational Logic Group at the University of Innsbruck. These include the termination tool TTT2, the confluence prover CSI, the completion tools mkbTT and KBCV, the complexity tool TcT, the strategy tool AutoStrat, as well as FORT, an implementation of the decision procedure for the first-order theory for a decidable class of rewrite systems. Besides its applications in research, this software pool has also proved invaluable for teaching, e.g., in multiple editions of the International Summer School on Rewriting.
