A tool implementation of the local inversion framework from Kirkeby and Glück [1]. The implementation includes four well-behaved rule-inverters ranging from trivial to full, partial and semi-inverters. For experimental and educational purposes.
The implementation of this framework and the associated diagnostics tool has been implemented by Maria Bendix Mikkelsen as part of a summer project. The code for the web-version is based on Claus Skou Nielsen and Michael Budde's Janus Playground, which can be found here.
Write a CCS program in the input text area. The tool recognizes the CoCo-format [2] as well as the format used in [1]. Examples CCSs can be loaded from the Example dropdown menu.
Before inverting, specify the function to be inverted and the io-set in Options.
To see the diagnostics of the CCS in the input window, click on the Diagnose button. Diagnostics will also be printed alongside inversions.
To print LaTeX code for the CCS in the input window, click on the Latex button.
Share is not working currently, in progress!
[1] Maja H. Kirkeby and Robert Glück (2020): "Inversion framework: reasoning about inversion by conditional term rewriting systems." In: Principles and Practice of Declarative Programming. Proceedings, ACM, p. Article 9.
[2] Confluence Competition CTRS format. http://project-coco.uibk.ac.at/problems/ctrs.php. Accessed: 2021-03-09.