Cláudia Nalon, Lan Zhang, Clare Dixon, and Ullrich Hustadt (2014a): A Resolution Prover for Coalition Logic

Cláudia Nalon, Lan Zhang, Clare Dixon, and Ullrich Hustadt (2014a): ``A Resolution Prover for Coalition Logic.'' In F.~Mogavero, A.~Murano and M.~Y.~Vardi, editors, Proceedings 2nd International Workshop on Strategic Reasoning (SR 2014), Electronic Proceedings in Theoretical Computer Science, 146:65--74, 2014.
Abstract, BibTeX, PDF.

We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency. The theorem prover CLProver is based on recent work on a resolution-based calculus for Coalition Logic that operates on coalition problems, a normal form for Coalition Logic. We provide an overview of coalition problems and of the resolution-based calculus for Coalition Logic. We then give details of the implementation of CLProver and present the results for a comparison with an existing tableau-based solver.