CARPA: Counter examples in Abstract Rewriting Produced Automatically

The tool Carpa automatically generates examples of finite abstract rewrite systems satisfying a given list of properties
The tool Carpa+ reads a similar list of properties, but instead generates a term rewriting system satisfying the given list of properties



Internally, first a SAT/SMT fomula is created representing the specified properties. Then the tool Yices is called for doing the real work. Finally, from the Yices output the desired output is created.

The following can be downloaded:

• A paper presenting the tool Carpa and the underlying theory (accepted for publication in Mathematical Structures in Computer Science).
• A manual presenting the input format of Carpa.
• A zip file containing source files and a Linux executable for Carpa. It also contains all examples from the paper.
• The paper Automatically finding particular term rewriting systems presenting the tool Carpa+ and the underlying theory.
• A zip file containing source files and a Linux executable for Carpa+ and all examples from the paper.

Last change: July 12, 2018