In this paper we introduce a calculus based on ordered resolution for Coalition Logic (CL), improving our previous approach based on unrefined resolution, and discuss the problems associated with imposing an ordering refinement in the context of CL. The calculus operates on `coalition problems', a normal form for CL where we use coalition vectors that can represent choices made by agents explicitly, and the inference rules of the calculus provide the basis for a decision procedure for the satisfiability problem in CL. We give correctness, termination and complexity results for our calculus. We also present experimental results for an implementation of the calculus and show that it outperforms a tableau-based decision procedure for Alternating-Time Temporal Logic (ATL) on two classes of benchmark formulae for CL.
For CLProver++, the prover for Coalition Logic introduced in this paper, and the benchmarks that were used see http://cgi.csc.liv.ac.uk/~ullrich/CLProver++/.[an error occurred while processing this directive]