Cynthia Kop and Naoki Nishida
Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450, pp. 549 – 557, 2015.
pdf 
doi:10.1007/978-3-662-48899-7_38
© Springer-Verlag Berlin Heidelberg 2015
Abstract
This paper discusses Ctrl, a tool to analyse – both automatically and manually – term rewriting with logical constraints. Ctrl can be used with TRSs on arbitrary underlying logics, and can automatically verify termination, confluence and (to a limited extent) term equivalence using inductive theorem proving. Ctrl also offers a manual mode for inductive theorem proving, allowing support for and verification of “hand-written” term equivalence proofs.
BibTex
@inproceedings{CKNN-LPAR15, author = "Cynthia Kop and Naoki Nishida", title = "Constrained Term Rewriting tooL", booktitle = "Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning", series = "Lecture Notes in Computer Science (Advanced Research in Computing and Software Science)", editor = "Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov", volume = 9450, pages = "549--557", year = 2015, doi = "10.1007/978-3-662-48899-7_38"}