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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.146.9 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |