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:



Last change: February 22, 2013