An inversion tool for conditional term rewriting systems – A case study of Ackermann inversion

Maria Bendix Mikkelsen, Robert Glück, Maja H. Kirkeby

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


We report on an inversion tool for a class of oriented conditional constructor term rewriting systems. Four well-behaved rule inverters ranging from trivial to full, partial and semi-inverters are included. Conditional term rewriting systems are theoretically well founded and can model functional and nonfunctional rewrite relations. We illustrate the inversion by experiments with full and partial inversions of the Ackermann function. The case study demonstrates, among others, that polyvariant inversion and input-output set propagation can reduce the search space of the generated inverse systems.

Original languageEnglish
Title of host publicationProceedings of the 9th International Workshop on Verification and Program Transformation
EditorsAlexei Lisitsa, Andrei P. Nemytykh
Number of pages9
Publication date6 Sep 2021
Publication statusPublished - 6 Sep 2021
Event9th International Workshop on Verification and Program Transformation, VPT 2021 - Virtual, Luxembourg, Luxembourg
Duration: 27 Mar 202128 Mar 2021


Conference9th International Workshop on Verification and Program Transformation, VPT 2021
CityVirtual, Luxembourg
SeriesElectronic Proceedings in Theoretical Computer Science, EPTCS


  • Case study
  • Program inversion
  • Program transformation
  • Term rewriting systems

Cite this