A Resolution Prover for Coalition Logic
This work addresses the need for efficient automated reasoning tools in cooperative agency for researchers and practitioners in logic and AI, but it is incremental as it builds on existing methods.
The authors tackled the problem of automated reasoning for Coalition Logic by developing a prototype theorem prover called CLProver, which is based on a resolution-based calculus and showed results in a comparison with an existing tableau-based solver.
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.