Tools in Term Rewriting for Education

Sarah Winkler
(Università di Verona, Italy)
Aart Middeldorp
(University of Innsbruck, Austria)

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.

In Pedro Quaresma, Walther Neuper and João Marcos: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software (ThEdu'19), Natal, Brazil, 25th August 2019, Electronic Proceedings in Theoretical Computer Science 313, pp. 54–72.
Published: 28th February 2020.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: