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"
}