A Resolution Prover for Coalition Logic

Cláudia Nalon
(Department of Computer Science, University of Brasília, Brazil)
Lan Zhang
(Information School Capital University of Economics and Business, China)
Clare Dixon
(Department of Computer Science, University of Liverpool, UK)
Ullrich Hustadt
(Department of Computer Science, University of Liverpool, UK)

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.

In Fabio Mogavero, Aniello Murano and Moshe Y. Vardi: Proceedings 2nd International Workshop on Strategic Reasoning (SR 2014), Grenoble, France, April 5-6, 2014, Electronic Proceedings in Theoretical Computer Science 146, pp. 65–73.
Published: 1st April 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.146.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org