CLProver++

CLProver++ is a resolution-based theorem prover for Coalition Logic implemented in C++ by Paul Gainer. It is based on an ordering refinement of the resolution calculus described in (Nalon, Zhang, Dixon and Hustadt, 2013). It accepts as input a set of DSNF_CL clauses and determines its satisfiability.

Below you find a download link for the source code for CLProver++ 1.0.3 which includes instructions on how to install and use the prover as well as some examples illustrating its input syntax.

CLProver++ is free software and is available under the GNU General Public License (version 2.0)

• CLProver++ 1.0.3: ZIP

We have conducted experiments on randomly generated Coalition Logic formulae of various structures in order to evaluate the effectiveness of CLProver++ and compared it with TATL and CLProver (Nalon, Zhang, Dixon and Hustadt, 2014). The formulae used in those experiments are available in TATL and CLProver++ format:

• Benchmark Class 1 -- CLProver++ syntax
• Benchmark Class 1 (layered modal translation) -- CLProver++ syntax
• Benchmark Class 1 -- TATL syntax
• Benchmark Class 2 -- CLProver++ syntax
• Benchmark Class 2 -- TATL syntax