Electronic Proceedings in Theoretical Computer Science (Apr 2014)

A Resolution Prover for Coalition Logic

  • Cláudia Nalon,
  • Lan Zhang,
  • Clare Dixon,
  • Ullrich Hustadt

DOI
https://doi.org/10.4204/eptcs.146.9
Journal volume & issue
Vol. 146, no. Proc. SR 2014
pp. 65 – 73

Abstract

Read online

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.