Nalon, Cláudia, Zhang, Lan, Dixon, Clare ORCID: 0000-0002-4610-9533 and Hustadt, Ullrich ORCID: 0000-0002-0455-0267
(2014)
A Resolution Prover for Coalition Logic.
In: 2nd International Workshop on Strategic Reasoning, Satellite workshop of ETAPS 2014.
Text
SR2014.9.pdf - Published version Download (492kB) |
Abstract
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.
Item Type: | Conference or Workshop Item (Unspecified) |
---|---|
Additional Information: | In Proceedings SR 2014, arXiv:1404.0414 |
Uncontrolled Keywords: | cs.LO, cs.LO, cs.AI, I.2.3;F.4.1 |
Depositing User: | Symplectic Admin |
Date Deposited: | 06 Jul 2017 13:07 |
Last Modified: | 19 Jan 2023 07:00 |
DOI: | 10.4204/eptcs.146.9 |
Related URLs: | |
URI: | https://livrepository.liverpool.ac.uk/id/eprint/3008348 |