@INPROCEEDINGS{Hustadt+Gainer+Dixon+Nalon+Zhang@TABLEAUX2015,
 AUTHOR        = {Hustadt, Ullrich and Gainer, Paul and Dixon, Clare and Nalon, Cl{\'a}udia and Zhang, Lan},
 TITLE         = {Ordered Resolution for Coalition Logic},
 PAGES         = {165-180},
 BOOKTITLE     = {Proceedings of the International Conference on
 Automated Reasoning with Analytic Tableaux and Related Methods 
 (TABLEAUX 2015) [Wroclaw, Poland, 20--24 September 2015]},
 YEAR          = {2015},
 EDITOR        = {de Nivelle, Hans},
 PUBLISHER     = {Springer International Publishing Switzerland},
 PADDRESS      = {Cham, Switzerland},
 PYEAR         = {2015},
 CADDRESS      = {Wroclaw, Poland},
 CYEAR         = {2015},
 CMONTH        = sep # {20--24},
 SERIES        = {LNAI},
 VOLUME        = {9323},
 URL           = {Hustadt+Gainer+Dixon+Nalon+Zhang@TABLEAUX2015.pdf},
 ABSTRACT      = {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.}
}