cl-banner

Constrained Term Rewriting tooL

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.

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.

 

  PDF |    doi:10.1007/978-3-662-48899-7_38  |  © Springer-Verlag Berlin Heidelberg 2015

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"
}
Nach oben scrollen