TTT2，带教学用终止模板
TTT2 with Termination Templates for Teaching
摘要：
一方面，手工检查特定的终止证明，比如使用特定的矩阵解释集合，可能是一项艰巨且容易出错的任务。另一方面，这种检查的自动化将节省时间，并有助于建立正确的考试解决方案，在课堂讲稿等，为此，我们引入了一个模板机制的终止工具TTT2，使我们能够限制某些终止方法的参数。在极端情况下，当所有参数都固定时，这样的限制会导致对特定证明的检查。
英文摘要：
On the one hand, checking specific termination proofs by hand, say using a particular collection of matrix interpretations, can be an arduous and error-prone task. On the other hand, automation of such checks would save time and help to establish correctness of exam solutions, examples in lecture notes etc. To this end, we introduce a template mechanism for the termination tool TTT2 that allows us to restrict parameters of certain termination methods. In the extreme, when all parameters are fixed, such restrictions result in checks for specific proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
